# How Our Compiler Learnt From Our Analyzers

## by Yannick Moy – May 22, 2015

Program analyzers interpret the source code of a program to compute some information. Hopefully, the way they interpret the program is consistent with the way that the compiler interprets it to generate an executable, or the information computed is irrelevant, possibly misleading. For example, if the analyzer says that there are no possible run-time errors in a program, and you rely on this information to compile with dynamic checking off, it is crucial that no run-time error could occur as a result of a divergence of opinion between the analyzer and the compiler on the meaning of an instruction.

At AdaCore, we're developing both the GNAT compiler and two source code analyzers, CodePeer and GNATprove, so we are very much aware of the need for a consistent interpretation of programs. In fact, we even try as much as possible to ensure that our analyzers are consistent with how other compilers besides GNAT interpret programs. In general, this means that we adapt our analyzers to how compilers behave, because it's easier to change our analyzers than to change all the existing Ada compilers.

But recently, we got a case which lead to a modification in the GNAT compiler. The issue was that GNAT interpreted different the value of the exponentiation expression A**B when B was statically known or not. To see that, take any version of GNAT prior to April, 20th 2015, and compile the following program with assertions (using -gnata):

procedure Exptest is
Static_B : constant := 3;

function Ident_Int (X : Integer) return Integer is (X);

procedure Test (A : Float) is
Dynamic_B : constant Integer := Ident_Int (Static_B);

V1 : constant Float := A ** Static_B;
V2 : constant Float := A ** Dynamic_B;
begin
pragma Assert (V1 = V2);
end Test;

F : Float := 0.5;
begin
while F < 1.0 loop
Test (F);
F := Float'Succ (F);
end loop;
end Exptest;

When running this program, you will get an assertion failure: