diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-06-30 15:59:25 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-06-30 15:59:25 +0200 |
| commit | 7bc2a5e6d2694f144e49fe60af6ddfd0e8a0aba0 (patch) | |
| tree | f964f94e326e13fc898cc997db24db87944cfcf0 /scheduling/BTL_SEsimuref.v | |
| parent | f03d8bc434ea992bd390b949c1e0ce7dd99d2ddc (diff) | |
| download | compcert-kvx-7bc2a5e6d2694f144e49fe60af6ddfd0e8a0aba0.tar.gz compcert-kvx-7bc2a5e6d2694f144e49fe60af6ddfd0e8a0aba0.zip | |
coercions and simplify
Diffstat (limited to 'scheduling/BTL_SEsimuref.v')
| -rw-r--r-- | scheduling/BTL_SEsimuref.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v index 9c84532b..66abe6e1 100644 --- a/scheduling/BTL_SEsimuref.v +++ b/scheduling/BTL_SEsimuref.v @@ -20,7 +20,7 @@ Record ristate := { (** [ris_smem] represents the current smem symbolic evaluations. (we also recover the history of smem in ris_smem) *) - ris_smem: smem; + ris_smem:> smem; (** For the values in registers: 1) we store a list of sval evaluations 2) we encode the symbolic regset by a PTree + a boolean indicating the default sval |