diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-03-05 11:02:51 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-03-05 11:04:50 +0100 |
| commit | 9833210392b7bddf740e6b555ce931efb46cf387 (patch) | |
| tree | f4be0845d40730fbb394b3c2474efe42e04a365d /mppa_k1c/abstractbb/AbstractBasicBlocksDef.v | |
| parent | cd69b24565713610d0ea5a613f4871af6e18e9d4 (diff) | |
| download | compcert-kvx-9833210392b7bddf740e6b555ce931efb46cf387.tar.gz compcert-kvx-9833210392b7bddf740e6b555ce931efb46cf387.zip | |
remove cumbersome dependency on genv in bblock_eq_test
Diffstat (limited to 'mppa_k1c/abstractbb/AbstractBasicBlocksDef.v')
| -rw-r--r-- | mppa_k1c/abstractbb/AbstractBasicBlocksDef.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v index 21e7bd98..904fb72c 100644 --- a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v +++ b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v @@ -29,6 +29,11 @@ Parameter genv: Type. (* environment to be used for evaluating an op *) *) Parameter op_eval: genv -> op -> list value -> option value. +Parameter is_constant: op -> bool. + +Parameter is_constant_correct: + forall ge o, is_constant o = true -> op_eval ge o nil <> None. + End LangParam. |