From e9076031a8f759b10606e8507490ed8c68b16a43 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 2 Jun 2020 19:06:27 +0100 Subject: Add proof to final_states --- src/verilog/HTL.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/verilog') diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index fffbb81..bf38b29 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. @@ -98,7 +98,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) := -- cgit