diff options
| author | James Pollard <james@pollard.dev> | 2020-06-03 15:29:54 +0100 |
|---|---|---|
| committer | James Pollard <james@pollard.dev> | 2020-06-03 15:29:54 +0100 |
| commit | 7e20d7bed643300605d9ff157d6dd206a7bb6b7b (patch) | |
| tree | 6139957c9b1f70715af635e99e713c621e403e6f /src/verilog/HTL.v | |
| parent | 88553f08d8f2ad96ae615e9648b7c1417573247a (diff) | |
| parent | e9076031a8f759b10606e8507490ed8c68b16a43 (diff) | |
| download | vericert-kvx-7e20d7bed643300605d9ff157d6dd206a7bb6b7b.tar.gz vericert-kvx-7e20d7bed643300605d9ff157d6dd206a7bb6b7b.zip | |
Merge branch 'develop' into arrays-proof
Diffstat (limited to 'src/verilog/HTL.v')
| -rw-r--r-- | src/verilog/HTL.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index 1ea0b1b..a553453 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -19,7 +19,7 @@ From Coq Require Import FSets.FMapPositive. From coqup Require Import Coquplib Value AssocMap. From coqup Require Verilog. -From compcert Require Events Globalenvs Smallstep Integers. +From compcert Require Events Globalenvs Smallstep Integers Values. From compcert Require Import Maps. Import HexNotationValue. @@ -109,7 +109,7 @@ Inductive initial_state (p: program): state -> Prop := Inductive final_state : state -> Integers.int -> Prop := | final_state_intro : forall retval retvali, - value_int_eqb retval retvali = true -> + retvali = valueToInt retval -> final_state (Returnstate retval) retvali. Definition semantics (m : program) := |