diff options
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. |