Open jlvargasme opened 5 months ago
The acc.zls file generates the following lines in the output of compilation:
acc.zls
[DEBUG] : return definition: (= vxf |42.0|) [DEBUG] : exception ignored: AstTranslationNotImplemented vc_gen_expression: Etuple [DEBUG] : Eseq : (e1 = |42.0| e2 = |42.0|)
[DEBUG] : Body exp :|42.0|
Where 42.0 is an undesired magic number in the code. This problem can cause issues in the verification conditions, since it adds an additional unrealistic constraint. Issue needs more investigation.
The
acc.zlsfile generates the following lines in the output of compilation:[DEBUG] : return definition: (= vxf |42.0|) [DEBUG] : exception ignored: AstTranslationNotImplemented vc_gen_expression: Etuple [DEBUG] : Eseq : (e1 = |42.0| e2 = |42.0|)
[DEBUG] : Body exp :|42.0|
Where 42.0 is an undesired magic number in the code. This problem can cause issues in the verification conditions, since it adds an additional unrealistic constraint. Issue needs more investigation.