diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2021-04-13 14:12:04 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-04-24 17:58:47 +0200 |
commit | ff88fc9f7b7a208555eace2ad0e7e8be753278b5 (patch) | |
tree | 12530c60ca36c0451e2530c16b0904e06551fa34 /flocq/Prop/Sterbenz.v | |
parent | 69e175746c27f340f544c329204d6ad030c3c347 (diff) | |
download | compcert-ff88fc9f7b7a208555eace2ad0e7e8be753278b5.tar.gz compcert-ff88fc9f7b7a208555eace2ad0e7e8be753278b5.zip |
More fixes for ld/std issue.
Volatile load and store are expanded later and also use the ld/std
instructions, therefore the same fixes that are applied as well for
them.
Bug 30983
Diffstat (limited to 'flocq/Prop/Sterbenz.v')
0 files changed, 0 insertions, 0 deletions