diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-08-19 14:44:34 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-08-19 14:44:34 +0100 |
| commit | e44054e439adfc2128e93e652178c6df42ee9159 (patch) | |
| tree | 57f299f94f16ae698efaf2fedc965f5a069f0534 /src/hls/HTL.v | |
| parent | 56f442f41aba4efb3929b79f15e5a4cc87579acb (diff) | |
| download | vericert-e44054e439adfc2128e93e652178c6df42ee9159.tar.gz vericert-e44054e439adfc2128e93e652178c6df42ee9159.zip | |
Find called module in Icall proof
Diffstat (limited to 'src/hls/HTL.v')
| -rw-r--r-- | src/hls/HTL.v | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 8d51750..d777d66 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -129,14 +129,10 @@ Qed. Definition genv := Globalenvs.Genv.t fundef unit. -Definition find_module (i: ident) (ge : genv) : option module := - match Globalenvs.Genv.find_symbol ge i with +Definition find_func {F V} (ge : Globalenvs.Genv.t F V) (symb : AST.ident) : option F := + match Globalenvs.Genv.find_symbol ge symb with | None => None - | Some b => - match Globalenvs.Genv.find_funct_ptr ge b with - | Some (AST.Internal f) => Some f - | _ => None - end + | Some b => Globalenvs.Genv.find_funct_ptr ge b end. Inductive stackframe : Type := @@ -208,7 +204,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := (Returnstate sf mid retval) | step_initcall : forall g callerid caller st asr asa sf callee_id callee callee_reset callee_params callee_param_vals, - find_module callee_id g = Some callee -> + find_func g callee_id = Some (AST.Internal callee) -> caller.(mod_externctrl)!callee_reset = Some (callee_id, ctrl_reset) -> (forall n param, nth_error callee_params n = Some param -> |