Mentions légales du service

Skip to content

Simplify projections applied to casted literals in VCs

Raphaël Rieu-Helft requested to merge simp_cast_projections into master

Function postconditions of the form result = x + 1 where result and x have type int32 results in verification conditions of the form:

int32'int result = int32'int x + int32'int (1:int32)

This PR is an attempt at simplifying it to int32'int result = int32'int x + 1.

TODO: update obsoleted sessions

Edited by Raphaël Rieu-Helft

Merge request reports