search

m-carrasco / TinyBCT

MIT License
3 stars 2 forks source link

Boolean-integer type compatibility. #65

Closed michael-emmi closed 5 years ago

michael-emmi commented 5 years ago

This assertion fails on the following program:

.class TestExceptionsWhen {
  .method void Main () cil managed {
    .locals init (bool)
      ldc.i4.1 
      stloc.0 
      ldloc.0 
      ldc.i4.0
      cgt.un 
      ret 
  }
}

The issue is that the arguments to the greater-than operation (cgt.un) are given incompatible Boogie types (int and bool) — the bool is due to the store and subsequent load to Boolean-typed local variable 0. In fact, this is valid CIL code (e.g., according to ECMA-335), since Boolean values are loaded onto the stack as zero-extended int32s. As far as I can tell, there are no relevant type-conversion operations here.

As far as context goes, this is a minimization of the code generated for the TestExceptionsWhen test on Mono, which is trips the assertion. I suppose that different code is being generated on Windows (?).

This code is based on code generated with this compiler:

$ csc 
Microsoft (R) Visual C# Compiler version 2.8.2.62916 (2ad4aabc)
Copyright (C) Microsoft Corporation. All rights reserved.
michael-emmi commented 5 years ago

This duplicates edgardozoppi/analysis-net#10.