aboutsummaryrefslogtreecommitdiffstats
path: root/common
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-02-03 19:14:25 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-02-03 19:14:25 +0100
commit65281dfbf2ce12f4fca5c1bfa57a14a429687ca7 (patch)
tree3c9630f44e92c903e97ee9f7e6bac645054e05ba /common
parent1dd98d18c57abdbc8dc50bbef729e8a898d55aad (diff)
downloadcompcert-kvx-65281dfbf2ce12f4fca5c1bfa57a14a429687ca7.tar.gz
compcert-kvx-65281dfbf2ce12f4fca5c1bfa57a14a429687ca7.zip
another version of proof that allows Vundef in loaded values
Diffstat (limited to 'common')
0 files changed, 0 insertions, 0 deletions