Ignore:
Timestamp:
Feb 8, 2013, 11:49:55 AM (8 years ago)
Author:
sacerdot
Message:

String type changed definition.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyFront.ma

    r2318 r2652  
    2020  λprefix:list labelled_instruction.λsigma:ppc_pc_map.
    2121  ∀i:ℕ.i < |prefix| →
    22   ¬is_jump (\snd (nth i ? prefix 〈None ?, Comment []〉)) →
     22  ¬is_jump (\snd (nth i ? prefix 〈None ?, Comment EmptyString〉)) →
    2323  \snd (bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉) = short_jump.
    2424 
     
    175175    [ None ⇒ False
    176176    | Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in
    177        pc1 = pc + instruction_size_jmplen j (\snd (nth n ? prefix 〈None ?, Comment []〉))
     177       pc1 = pc + instruction_size_jmplen j (\snd (nth n ? prefix 〈None ?, Comment EmptyString〉))
    178178    ]
    179179  ].
     
    193193         (λppc.bitvector_of_nat ? (\fst (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))
    194194         (λppc.jmpeqb long_jump (\snd (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))
    195          (bitvector_of_nat ? n) (\snd (nth n ? program 〈None ?, Comment []〉))
     195         (bitvector_of_nat ? n) (\snd (nth n ? program 〈None ?, Comment EmptyString〉))
    196196    ]
    197197  ].
     
    227227  λprefix:list labelled_instruction.λsigma:ppc_pc_map.
    228228  ∀i.i < |prefix| →
    229   let 〈label,instr〉 ≝ nth i ? prefix 〈None ?, Comment []〉 in
     229  let 〈label,instr〉 ≝ nth i ? prefix 〈None ?, Comment EmptyString〉 in
    230230  (\snd (bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉) = short_jump →
    231231    bool_to_Prop (¬is_call instr)) ∧
     
    565565definition nec_plus_ultra ≝
    566566  λprogram:list labelled_instruction.λp:ppc_pc_map.
    567   ¬(∀i.i < |program| → is_jump (\snd (nth i ? program 〈None ?, Comment []〉)) →
     567  ¬(∀i.i < |program| → is_jump (\snd (nth i ? program 〈None ?, Comment EmptyString〉)) →
    568568  \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,short_jump〉) = long_jump).
    569569 
     
    627627        type *)
    628628      cut (instruction_size_jmplen jl
    629        (\snd (nth i ? program 〈None ?, Comment []〉)) =
     629       (\snd (nth i ? program 〈None ?, Comment EmptyString〉)) =
    630630       instruction_size … (bitvector_of_nat ? i)
    631        (\snd (nth i ? program 〈None ?, Comment []〉)))
     631       (\snd (nth i ? program 〈None ?, Comment EmptyString〉)))
    632632      [6: #H <H @Hcp_unsafe
    633633      |5: whd in match (instruction_size_jmplen ??);
     
    635635          whd in match (assembly_1_pseudoinstruction …);
    636636          whd in match (expand_pseudo_instruction …);
    637           normalize nodelta inversion (nth i ? program 〈None ?,Comment []〉) in Hsafe;
     637          normalize nodelta inversion (nth i ? program 〈None ?,Comment EmptyString〉) in Hsafe;
    638638          #lbl #instr cases instr
    639639          [1: #pi normalize nodelta cases pi
     
    696696                [1,5,9,13,17,21,25,29,33,37,41:
    697697                  whd in match fetch_pseudo_instruction; normalize nodelta
    698                   >(nth_safe_nth … 〈None ?, Comment []〉) >nat_of_bitvector_bitvector_of_nat_inverse
     698                  >(nth_safe_nth … 〈None ?, Comment EmptyString〉) >nat_of_bitvector_bitvector_of_nat_inverse
    699699                  [1: >Hnth_eq in ⊢ (??%?);
    700700                  |3: >Hnth_eq in ⊢ (??%?);
Note: See TracChangeset for help on using the changeset viewer.