Practical-Formal-Methods / adiff

Tool for differentially testing soundness and precision of program analyzers
MIT License
11 stars 6 forks source link

Type annotator #120

Open chkl opened 6 years ago

chkl commented 6 years ago

This adds a new typechecker to vdiff. Currently the type information on expressions is correct most of the time, but there is at least one bug relating to "long long" types. More interestingly, for simplification reasons I changed the definition of AnnTranslationUnit SemPhase to not include the GlobalDecls as an annotation anymore (it was never needed anyway). It seems like that this was the piece of cylic datatype (or computation?) that caused the crashes.

So this means that this typechecker here is probably superfluous.