Changeset 2645 for src/Clight


Ignore:
Timestamp:
Feb 7, 2013, 9:22:22 PM (8 years ago)
Author:
sacerdot
Message:
  1. some broken back-end files repaires, several still to go
  2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
  3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
Location:
src/Clight
Files:
15 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r2608 r2645  
    99definition P_res: ∀A.∀P:A → Prop.res A → Prop ≝
    1010  λA,P,a. match a with [ Error _ ⇒ True | OK v ⇒ P v ].
    11 
    12 axiom ValueIsNotABoolean : String.
    1311
    1412definition exec_bool_of_val : ∀v:val. ∀ty:type. res bool ≝
     
    6462#A #B #P #m #e #f elim e; normalize; /2/; qed.
    6563
    66 
    67 axiom BadCast : String. (* TODO: refine into more precise errors? *)
    6864
    6965definition try_cast_null : ∀m:mem. ∀sz. ∀i:BitVector (bitsize_of_intsize sz). ∀ty:type. ∀ty':type. res val  ≝
     
    151147definition load_value_of_type' ≝
    152148λty,m,l. let 〈loc,ofs〉 ≝ l in load_value_of_type ty m loc ofs.
    153 
    154 axiom BadlyTypedTerm : String.
    155 axiom UnknownIdentifier : String.
    156 axiom BadLvalueTerm : String.
    157 axiom FailedLoad : String.
    158 axiom FailedOp : String.
    159149
    160150(* To make the evaluation of bare lvalue expressions invoke exec_lvalue with
     
    317307].
    318308
    319 axiom WrongNumberOfParameters : String.
    320 axiom FailedStore : String.
    321 
    322309(* TODO: can we establish that length params = length vs in advance? *)
    323310let rec exec_bind_parameters (e:env) (m:mem) (params:list (ident × type)) (vs:list val) on params : res mem ≝
     
    358345let 〈loc,ofs〉 ≝ l in
    359346  store_value_of_type ty m loc ofs v.
    360 
    361 axiom NonsenseState : String.
    362 axiom ReturnMismatch : String.
    363 axiom UnknownLabel : String.
    364 axiom BadFunctionValue : String.
    365347
    366348let rec exec_step (ge:genv) (st:state) on st : (IO io_out io_in (trace × state)) ≝
     
    531513].
    532514
    533 axiom MainMissing : String.
    534 
    535515definition make_global : clight_program → genv ≝
    536516λp. globalenv … (fst ??) p.
  • src/Clight/Csyntax.ma

    r2468 r2645  
    496496Open Local Scope string_scope.
    497497*)
    498 axiom UnknownField : String.
    499498
    500499let rec field_offset_rec (id: ident) (fld: fieldlist) (pos: nat)
  • src/Clight/TypeComparison.ma

    r2468 r2645  
    22include "Clight/Csyntax.ma".
    33include "utilities/extranat.ma".
    4 
    5 axiom TypeMismatch : String.
    64
    75definition sz_eq_dec : ∀s1,s2:intsize. (s1 = s2) + (s1 ≠ s2).
  • src/Clight/test/addptrcharboth.test.ma

    r2619 r2645  
    3838include "RTLabs/CostCheck.ma".
    3939
    40 axiom MISSING:String.
    41 axiom EXTERNAL:String.
    42 
    4340definition readable_body ≝
    4441λfn. insert_sort ?
  • src/Clight/test/badconditional.test.ma

    r2619 r2645  
    3939include "RTLabs/CostCheck.ma".
    4040
    41 axiom MISSING:String.
    42 axiom EXTERNAL:String.
    43 
    4441definition readable_body ≝
    4542λfn. insert_sort ?
  • src/Clight/test/controlflow.test.ma

    r2619 r2645  
    3737
    3838include "RTLabs/CostCheck.ma".
    39 
    40 axiom MISSING:String.
    41 axiom EXTERNAL:String.
    4239
    4340definition readable_body ≝
  • src/Clight/test/endptr.test.ma

    r2619 r2645  
    3333
    3434include "RTLabs/CostCheck.ma".
    35 
    36 axiom MISSING:String.
    37 axiom EXTERNAL:String.
    3835
    3936definition readable_body ≝
  • src/Clight/test/endptr2.test.ma

    r2619 r2645  
    3333
    3434include "RTLabs/CostCheck.ma".
    35 
    36 axiom MISSING:String.
    37 axiom EXTERNAL:String.
    3835
    3936definition readable_body ≝
  • src/Clight/test/forcont.test.ma

    r2619 r2645  
    3737
    3838include "RTLabs/CostCheck.ma".
    39 
    40 axiom MISSING:String.
    41 axiom EXTERNAL:String.
    4239
    4340definition readable_body ≝
  • src/Clight/test/goto-if.test.ma

    r2619 r2645  
    4545include "RTLabs/CostCheck.ma".
    4646
    47 axiom MISSING:String.
    48 axiom EXTERNAL:String.
    49 
    5047definition readable_body ≝
    5148λfn. insert_sort ?
  • src/Clight/test/implicit.test.ma

    r2619 r2645  
    3838include "RTLabs/CostCheck.ma".
    3939
    40 axiom MISSING:String.
    41 axiom EXTERNAL:String.
    42 
    4340definition readable_body ≝
    4441λfn. insert_sort ?
  • src/Clight/test/implicitcond.test.ma

    r2619 r2645  
    3838include "RTLabs/CostCheck.ma".
    3939
    40 axiom MISSING:String.
    41 axiom EXTERNAL:String.
    42 
    4340definition readable_body ≝
    4441λfn. insert_sort ?
  • src/Clight/test/sum.test.ma

    r2619 r2645  
    3737
    3838include "RTLabs/CostCheck.ma".
    39 
    40 axiom MISSING:String.
    41 axiom EXTERNAL:String.
    4239
    4340definition readable_body ≝
  • src/Clight/test/trivial.test.ma

    r2619 r2645  
    3737
    3838include "RTLabs/CostCheck.ma".
    39 
    40 axiom MISSING:String.
    41 axiom EXTERNAL:String.
    4239
    4340definition readable_body ≝
  • src/Clight/toCminor.ma

    r2601 r2645  
    8585definition var_types ≝ identifier_map SymbolTag (var_type × type).
    8686
    87 axiom UndeclaredIdentifier : String.
    88 
    8987definition lookup' ≝
    9088λvars:var_types.λid. opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id).
     
    249247
    250248alias id "CMexpr" = "cic:/matita/cerco/Cminor/Cminor_syntax/expr.ind(1,0,0)".
    251 
    252 axiom BadlyTypedAccess : String.
    253 axiom BadLvalue : String.
    254 axiom MissingField : String.
    255249
    256250(* type_should_eq enforces that two types are equal and eliminates this equality by
     
    605599λP,r1,r2,e. check_region r1 r2 (λr.Σe:CMexpr (ASTptr r).expr_vars ? e P) e.
    606600*)
    607 axiom FIXME : String.
    608601
    609602(* Given a source and target type, translate an expession of type source to type target *)
     
    941934definition lenv ≝ identifier_map SymbolTag (identifier Label).
    942935
    943 axiom MissingLabel : String.
    944 
    945936(* Find the Cminor label corresponding to [l] or fail. *)
    946937definition lookup_label ≝
     
    11791170  return_ok rettyp s' ∧                           (* return statements have correct typ *)
    11801171  label_wf s s' lbls flag.                        (* labels are "properly" declared, as defined in [ŀabel_wf].*)
    1181 
    1182 axiom ReturnMismatch : String.
    11831172
    11841173let rec translate_statement (vars:var_types) (uv:tmpgen vars) (ul:labgen) (lbls:lenv) (flag:convert_flag) (rettyp:option typ) (s:statement) on s
     
    15081497] qed.
    15091498
    1510 axiom ParamGlobalMixup : String.
    1511 
    15121499(* params and statement aren't real parameters, they're just there for giving the invariant. *)
    15131500definition alloc_params :
     
    15331520@(expr_vars_mp … (tmp_preserved … uv1)) whd >E @refl
    15341521qed.
    1535 
    1536 axiom DuplicateLabel : String.
    15371522
    15381523definition lenv_list_inv : lenv → lenv → list ident → Prop ≝
Note: See TracChangeset for help on using the changeset viewer.