Fábio Pakk Selmi-Dei

icon indicating a website link https://www.linkedin.com/in/fabio-pakk-selmi-dei-08a5195/

icon company Cocotec icon location United Kingdom icon location Computer scientist specialized in the development of programming languages and tools such as compilers, static analyzers and formal verifiers. Expert in C++.

Results 3 issues of Fábio Pakk Selmi-Dei

"Packaging wand might fail" in Viper online example

1 comment

Carbon is emitting the following messages for the program in attachment: - Packaging wand might fail. Assertion elems(l1) == old(elems(l1)[..index]) ++ old[lhs](elems(tmp)) might not hold. - Postcondition of appendit_wand might...

magic-wands

Macro containing calls to other macros might cause location issues

The following code is causing issues in the correct line: ``` define A() false define B() A() method test() { assert B() // Issue in this line, not in the...

Improve support for Magic Wands in both backends

At the moment, Magic Wands are not entirely supported in function preconditions and in predicates. As discussed on several issues (viperproject/carbon#364, #456, viperproject/carbon#244), it was decided to disable support for...