diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-12 12:41:28 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-12 12:41:28 +0100 |
| commit | 935dcae6384e718d26d29377e4c50e53151809e4 (patch) | |
| tree | 7f01f1f8f03101c8e99f0fc68becd183d7d54378 /backend/CSE3analysis.v | |
| parent | a3be6358778bb02b03b62486a60b9fd9ef1f1c04 (diff) | |
| download | compcert-kvx-935dcae6384e718d26d29377e4c50e53151809e4.tar.gz compcert-kvx-935dcae6384e718d26d29377e4c50e53151809e4.zip | |
store sound
Diffstat (limited to 'backend/CSE3analysis.v')
| -rw-r--r-- | backend/CSE3analysis.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index a85cd493..300bb216 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -296,6 +296,11 @@ Section OPERATIONS. end else rel'. + Definition store + (chunk : memory_chunk) (addr: addressing) (args : list reg) + (src : reg) (ty: typ) + (rel : RELATION.t) : RELATION.t := + store1 chunk addr (forward_move_l rel args) src ty rel. End PER_NODE. Definition apply_instr no instr (rel : RELATION.t) : RB.t := |