Are Spark pre condition results usually warnings?

General
1

I have a procedure with an argument

STM32.Timers.Run.Set_Counter 
(Timer : STM32.Devices.Timers.Timer_T; 
Value => 16#FFFF_00FF#);

It has a contract

with Pre => Timer in
STM32.Devices.Timers.Counter_16_Bit
 and then Value <= 16#FFFF#;

It is flagged during proving but only as a warning of precondition might fail, cannot prove Value <= 16#FFFF#

Okay so great but why is it just a warning instead of something like Error: precondition failed?

Edit: Actually I think I read about a SPARK update separating errors and warnings more distinctly but shouldn’t it be more strongly worded than might fail?

2

AFAIK, an error is something that SPARK can prove to be wrong or that is wrong by SPARK’s Reference Manual (incorrect syntax). Warnings are that SPARK has not proven it to be wrong, but it has not proven it to be fully right.

The way I fix warnings is by improving contracts and or types that may allow SPARK to reason better about the program or, easily and with great success, by increasing the prove limit, time limit and iterations limit so that SPARK may be able to prove all values. SPARK in this case may not have a smart way of proving your contract so it is bruteforcing it, most likely having to test all 16#FFFF# values…

I hope it helps,
Fer

3

hmmm. I didn’t write the procedure parameter input like a signature for some reason above which might be confusing but I am basically putting a value which breaches the pre condition as a parameter input. It found it but I was just expecting a bit of a louder perhaps red highlighting instead of might fail and orange highlighting as I believe it obviously fails the pre condition. I guess I should try a single argument without any static predicates on timer selection and see what that looks like.

4

What if you change the order of the and then parameters in the precondition. Does that change it into a warning? Also, make sure that your prove level is high enough for SPARK to check more than the syntax and basic things :slight_smile:

5

Ok, so your precondition is Value <= 16#FFFF#
But your call(?) to Set_Counter is 16#FFFF_00FF#?
(The syntax seems like a mismash of named-parameter association in a call, and declaration.)

What is the type of Value?
Unsigned, or signed? If unsigned, modular, or not?

If you can, try constraining the problem-space that the prover has to check: this reduces the combinatoric-explosion.

Oh, ok.
First off, the and then is the operation that precludes optimization (like or else) —if Divisor /= 0 and then …— so you are telling the prover that Timer in Counter_16_bit and then stuff. IIUC, this is equivalent to saying (for all X in Counter_16_Bit => Value <= 16#FFFF#), so you might be forcing the combinatoric-explosion.

Id’s decouple the temporal portion of the logic, if you can, and then perhaps try “rephrasing” your condition if it persists. One thing that’s useful for debugging verification condition failures, is to “by parts” until you get/isolate the problematic clause. — It’s been a while, but last time I used SPARK, there were a few “easy to say” conditionals that it choked on which had to be restated/reformulated in order to be checkable. (If sufficiently complex, you can use ghost-code, too.)

1 Like
6

When I just have the Value precondition then it says medium: precondition might fail without the cannot prove Value <= 16#FFFF# line. With the and then it just says medium: precondition might fail. Seems like I was wrong about it being a warning :person_facepalming:. I guess I saw it in the same color among other warnings.

I’m also seeing medium: predicate check might fail in another place which might explain the issue I have had with predicates but then why is it choosing the wrong overloaded procedure instead of saying it’s ambiguous. It is receiving a 16 bit timer as a base enum type but choosing the 32 bit procedure.

I thought you could do.

type Timer_T := (One, Two, Three);

subtype Timer_16 is Timer_T with
Static_Predicate => Timer_16 in Two;

subtype Timer_32 is Timer_T with
Static_Predicate => Timer_32 
not in Timer_16;

Set_Counter (Timer => Timer_16;
      Value => Unsigned_16);

Set_Counter (Timer => Timer_32;
       Value => Unsigned_32);

Timer : constant Timer_T := Two;
Set_Counter (Timer, 16#ffff#);

That seems to not select the right overloaded procedure though. Does Timer have to be.

Timer : constant Timer_16 := Two;
7

It’s cool that you can use predicates with Spark pre condition proving in any case.

I actually needed

Pre => 
((Timer in STM32.Devices.Timers.Counter_16_Bit)
 and then Value <= 16#FFFF#)
 or else Timer not in STM32.Devices.Timers.Counter_16_Bit;

Though it’s still confusing that it says precondition might fail instead of fails :thinking:. I guess just the language from dealing with false positives.

8

There’s an option to generate/display the counterexample.
Sometimes it shows a “hole” in your reasoning, sometimes the prover doesn’t have the information to prove; in the latter case, there are some pragmas/techniques to address that, though I don’t remember where I stumbled across the website/tutorial to show how to do it.

Have you tried omitting the parameter, using the correct one via overload?

Package Example is
  Type Enumeration is ( A, B, C );
  Procedure Set( Object : Integer_32 );
  Procedure Set( Object : Integer_64 );
Private
  Procedure Set( Object : Integer_32 ) is ( Internal_Set(A, Object) );
  Procedure Set( Object : Integer_64 ) is ( Internal_Set(B, Object) );
End Example;

Or, wait… are you trying to model the HW aspect of the timers?