Changeset 11 for C-semantics
- Timestamp:
- Jul 7, 2010, 12:55:01 PM (11 years ago)
- Location:
- C-semantics
- Files:
-
- 4 edited
Legend:
- Unmodified
- Added
- Removed
-
C-semantics/Cexec.ma
r10 r11 322 322 and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (Σr:block × int. eval_lvalue ge en m (Expr e' ty) (\fst r) (\snd r)) ≝ 323 323 match e' with 324 [ Evar id ⇒ Some ? ( 325 l ← opt_to_res ? (get ? PTree ? id en);: 326 OK ? 〈l, zero〉) 324 [ Evar id ⇒ 325 match (get ? PTree ? id en) with 326 [ None ⇒ Some ? (l ← opt_to_res ? (find_symbol Genv ? ge id);: OK ? 〈l,zero〉) (* global *) 327 | Some l ⇒ Some ? (OK ? 〈l,zero〉) (* local *) 328 ] 327 329 | Ederef a ⇒ Some ? ( 328 330 v ← exec_expr ge en m a;: … … 336 338 match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ]. 337 339 nwhd; //; 338 ##[ napply sig_bind2_OK; nrewrite > c 2; nrewrite > c4; #loc ofs H;340 ##[ napply sig_bind2_OK; nrewrite > c4; #loc ofs H; 339 341 napply opt_OK; #v ev; /2/; 340 ##| napply sig_bind2_OK; nrewrite > c 2; nrewrite > c4; #loc ofs H;342 ##| napply sig_bind2_OK; nrewrite > c4; #loc ofs H; 341 343 napply opt_OK; #v ev; /2/; 342 344 ##| napply sig_bind2_OK; #loc ofs H; … … 355 357 ##| napply (eval_Econdition_false … Hvb ? Hv); napply (bool_of ??? Hb); 356 358 ##] 357 ##| napply opt_bind_OK; #l el; napply eval_Evar_local; // 359 ##| napply opt_bind_OK; #l el; napply eval_Evar_global; /2/; 360 ##| napply eval_Evar_local; /2/ 358 361 ##| napply sig_bind_OK; #v; ncases v; //; #l ofs ev Hv; nwhd; 359 362 napply eval_Ederef; // … … 555 558 | _ ⇒ Some ? (Error ?) 556 559 ] 557 | _ ⇒ Some ? (Error ?) 560 | Returnstate res k m ⇒ 561 match k with 562 [ Kcall r f e k' ⇒ 563 match r with 564 [ None ⇒ 565 match res with 566 [ Vundef ⇒ Some ? (OK ? 〈E0, (State f Sskip k' e m)〉) 567 | _ ⇒ Some ? (Error ?) 568 ] 569 | Some r' ⇒ 570 match r' with [ mk_pair locofs ty ⇒ 571 match locofs with [ mk_pair loc ofs ⇒ Some ? ( 572 m' ← opt_to_res ? (store_value_of_type ty m loc ofs res);: 573 OK ? 〈E0, (State f Sskip k' e m')〉) 574 ] 575 ] 576 ] 577 | _ ⇒ Some ? (Error ?) 578 ] 558 579 ]. nwhd; //; 559 580 ##[ nrewrite > c7; napply step_skip_call; //; napply c8; … … 580 601 napply sig_bind_OK; #m2 em1 Hbind; 581 602 nwhd; napply (step_internal_function … Halloc Hbind); 603 ##| napply opt_bind_OK; #m' em'; napply step_returnstate_1; //; 582 604 ##] 583 605 nqed. -
C-semantics/Maps.ma
r10 r11 185 185 naxiom assoc_remove: ∀A: Type. ident → list (ident × A) → list (ident × A). 186 186 naxiom assoc_tree_map: ∀A,B: Type. (ident → A → B) → list (ident × A) → list (ident × B). 187 n axiom assoc_elements: ∀A: Type. list (ident × A) → list (ident × A).187 ndefinition assoc_elements: ∀A: Type. list (ident × A) → list (ident × A) ≝ λA,x.x. 188 188 naxiom assoc_tree_fold: ∀A,B: Type. (B → ident → A → B) → list (ident × A) → B → B. 189 189 -
C-semantics/compcert-1.7.1-matita.patch
r9 r11 1 diff -N --exclude=Configuration.ml --exclude=test --exclude=runtime --exclude='*~' --exclude=extraction --exclude=Makefile.config --exclude=ccomp --exclude=_build --exclude='*.vo' --exclude='*.glob' -ur compcert-1.7.1/cfrontend/PrintMatitaSyntax.ml compcert-1.7.1-matitaout/cfrontend/PrintMatitaSyntax.ml1 diff -N '--exclude=Configuration.ml' '--exclude=test' '--exclude=runtime' '--exclude=*~' '--exclude=extraction' '--exclude=Makefile.config' '--exclude=ccomp' '--exclude=_build' '--exclude=*.vo' '--exclude=*.glob' -ur compcert-1.7.1/cfrontend/PrintMatitaSyntax.ml compcert-1.7.1-matitaout/cfrontend/PrintMatitaSyntax.ml 2 2 --- compcert-1.7.1/cfrontend/PrintMatitaSyntax.ml 1970-01-01 01:00:00.000000000 +0100 3 +++ compcert-1.7.1-matitaout/cfrontend/PrintMatitaSyntax.ml 2010-0 6-15 10:36:33.000000000 +01003 +++ compcert-1.7.1-matitaout/cfrontend/PrintMatitaSyntax.ml 2010-07-07 09:51:45.000000000 +0100 4 4 @@ -0,0 +1,471 @@ 5 5 +(* *********************************************************************) … … 144 144 + | Tfunction(args, res) -> "(Tfunction " ^ typelist args ^ " " ^ stype res ^ ")" 145 145 + | Tstruct(name, fld) -> 146 + fieldlist "(Tstruct " name fld146 + fieldlist "(Tstruct (succ_pos_of_nat " name fld 147 147 + | Tunion(name, fld) -> 148 + fieldlist "(Tunion " name fld148 + fieldlist "(Tunion (succ_pos_of_nat " name fld 149 149 + | Tcomp_ptr name -> 150 + "(Tcomp_ptr " ^ Int32.to_string (camlint_of_positive name) ^ ")"150 + "(Tcomp_ptr (succ_pos_of_nat " ^ Int32.to_string (camlint_of_positive name) ^ "))" 151 151 + and typelist l = 152 152 + let b = Buffer.create 20 in … … 165 165 + Buffer.add_string b s; 166 166 + Buffer.add_string b (Int32.to_string (camlint_of_positive name)); 167 + Buffer.add_ char b ' ';167 + Buffer.add_string b ") "; 168 168 + let rec add_fields = function 169 169 + | Fnil -> Buffer.add_string b "Fnil" 170 170 + | Fcons(id, ty, tl) -> 171 + Buffer.add_string b "(Fcons ";171 + Buffer.add_string b "(Fcons (succ_pos_of_nat "; 172 172 + Buffer.add_string b (Int32.to_string (camlint_of_positive id)); 173 + Buffer.add_ char b ' ';173 + Buffer.add_string b ") "; 174 174 + Buffer.add_string b (stype ty); 175 175 + Buffer.add_char b ' '; … … 193 193 + fprintf p "(Econst_float %F)" f 194 194 + | Evar id -> 195 + fprintf p "(Evar %ld)" (camlint_of_positive id)195 + fprintf p "(Evar (succ_pos_of_nat %ld))" (camlint_of_positive id) 196 196 + | Eunop(op, e1) -> 197 197 + fprintf p "(Eunop %s %a)" (name_unop op) print_expr e1 … … 225 225 + fprintf p "(Esizeof %s)" (stype ty) 226 226 + | Efield(e1, id) -> 227 + fprintf p "(Efield %a %li)" print_expr e1 (camlint_of_positive id)227 + fprintf p "(Efield %a (succ_pos_of_nat %li))" print_expr e1 (camlint_of_positive id) 228 228 + end; 229 229 + fprintf p " %s)@]" (stype ty) … … 286 286 + fprintf p "(Sreturn (Some ? %a))" print_expr e 287 287 + | Slabel(lbl, s1) -> 288 + fprintf p "(Slabel %li@ %a)" (camlint_of_positive lbl) print_stmt s1288 + fprintf p "(Slabel (succ_pos_of_nat %li)@ %a)" (camlint_of_positive lbl) print_stmt s1 289 289 + | Sgoto lbl -> 290 + fprintf p "(Sgoto %li)" (camlint_of_positive lbl)290 + fprintf p "(Sgoto (succ_pos_of_nat %li))" (camlint_of_positive lbl) 291 291 + 292 292 +and print_cases p cases = … … 307 307 + | Coq_pair(id, ty) :: rem -> 308 308 + if not first then Buffer.add_string b "; "; 309 + Buffer.add_string b "mk_pair ?? ";309 + Buffer.add_string b "mk_pair ?? (succ_pos_of_nat "; 310 310 + Buffer.add_string b (Int32.to_string (camlint_of_positive id)); 311 + Buffer.add_ char b ' ';311 + Buffer.add_string b ") "; 312 312 + Buffer.add_string b (stype ty); 313 313 + add_params false rem in … … 324 324 + 325 325 +let print_fundef p (Coq_pair(id, fd)) = 326 + fprintf p "@[<v 2>mk_pair ?? %li" (camlint_of_positive id);326 + fprintf p "@[<v 2>mk_pair ?? (succ_pos_of_nat %li) " (camlint_of_positive id); 327 327 + match fd with 328 328 + | External(id', args, res) -> 329 + fprintf p "(External %li%s %s)@]" (camlint_of_positive id) (typelist args) (stype res)329 + fprintf p "(External (succ_pos_of_nat %li) %s %s)@]" (camlint_of_positive id) (typelist args) (stype res) 330 330 + | Internal f -> 331 331 + fprintf p "(Internal (@ %a@;<0 -2>))@]" print_function f … … 360 360 + 361 361 +let print_globvar p (Coq_pair(Coq_pair(id, init), ty)) = 362 + fprintf p "@[<hov 2>(mk_pair ?? (mk_pair ?? %li@ %a)@ %s)@]"362 + fprintf p "@[<hov 2>(mk_pair ?? (mk_pair ?? (succ_pos_of_nat %li)@ %a)@ %s)@]" 363 363 + (camlint_of_positive id) 364 364 + (print_list print_init) init … … 469 469 + StructUnionSet.iter (print_struct_or_union p) !struct_unions;*) 470 470 + print_list print_fundef p prog.prog_funct; 471 + fprintf p "@\n %li@\n" (camlint_of_positive (Hashtbl.find atom_of_string "main"));471 + fprintf p "@\n(succ_pos_of_nat %li)@\n" (camlint_of_positive (Hashtbl.find atom_of_string "main")); 472 472 + print_list print_globvar p prog.prog_vars; 473 473 + fprintf p "@;<0 -2>.@]@." 474 474 + 475 475 + 476 diff -N --exclude=Configuration.ml --exclude=test --exclude=runtime --exclude='*~' --exclude=extraction --exclude=Makefile.config --exclude=ccomp --exclude=_build --exclude='*.vo' --exclude='*.glob' -ur compcert-1.7.1/driver/Clflags.ml compcert-1.7.1-matitaout/driver/Clflags.ml476 diff -N '--exclude=Configuration.ml' '--exclude=test' '--exclude=runtime' '--exclude=*~' '--exclude=extraction' '--exclude=Makefile.config' '--exclude=ccomp' '--exclude=_build' '--exclude=*.vo' '--exclude=*.glob' -ur compcert-1.7.1/driver/Clflags.ml compcert-1.7.1-matitaout/driver/Clflags.ml 477 477 --- compcert-1.7.1/driver/Clflags.ml 2010-03-03 13:22:44.000000000 +0000 478 478 +++ compcert-1.7.1-matitaout/driver/Clflags.ml 2010-06-14 15:50:27.000000000 +0100 … … 485 485 let option_E = ref false 486 486 let option_S = ref false 487 diff -N --exclude=Configuration.ml --exclude=test --exclude=runtime --exclude='*~' --exclude=extraction --exclude=Makefile.config --exclude=ccomp --exclude=_build --exclude='*.vo' --exclude='*.glob' -ur compcert-1.7.1/driver/Driver.ml compcert-1.7.1-matitaout/driver/Driver.ml487 diff -N '--exclude=Configuration.ml' '--exclude=test' '--exclude=runtime' '--exclude=*~' '--exclude=extraction' '--exclude=Makefile.config' '--exclude=ccomp' '--exclude=_build' '--exclude=*.vo' '--exclude=*.glob' -ur compcert-1.7.1/driver/Driver.ml compcert-1.7.1-matitaout/driver/Driver.ml 488 488 --- compcert-1.7.1/driver/Driver.ml 2010-03-30 13:19:52.000000000 +0100 489 489 +++ compcert-1.7.1-matitaout/driver/Driver.ml 2010-06-14 15:51:34.000000000 +0100 -
C-semantics/extralib.ma
r10 r11 267 267 ##] nqed. 268 268 269 naxiom Z_times : Z → Z → Z. 269 ndefinition Z_times : Z → Z → Z ≝ 270 λx,y. match x with 271 [ OZ ⇒ OZ 272 | pos n ⇒ 273 match y with 274 [ OZ ⇒ OZ 275 | pos m ⇒ pos (n*m) 276 | neg m ⇒ neg (n*m) 277 ] 278 | neg n ⇒ 279 match y with 280 [ OZ ⇒ OZ 281 | pos m ⇒ neg (n*m) 282 | neg m ⇒ pos (n*m) 283 ] 284 ]. 270 285 interpretation "integer multiplication" 'times x y = (Z_times x y). 271 286
Note: See TracChangeset
for help on using the changeset viewer.