TruncDiv applied to permission values crashes VerCors

[superaxander]

The Java, C, and C++ frontends encode the division operator / as truncating division. If you use this operator to divide a permission value this crashes vercors.

C test file:

int f;

//@ requires Perm(f, write/2);
void foo() {
}

Java test file:

class Min {
    static int f;

    //@ requires Perm(f, write/2);
    void foo() {
    }
}

The error

viper.api.backend.SilverBackend$ConsistencyErrors: The silver AST delivered to viper is not valid:                                                                                                                                                              
 - Consistency error: Function truncdiv with formal arguments List(a: Int, b: Int) cannot be applied to provided arguments List(write, 2). (/home/alexander/vercors/min.java-4-26--4-33;unique_id=105)                                                          
 - Consistency error: Function truncdiv with formal arguments List(a: Int, b: Int) cannot be applied to provided arguments List(write, 2). (/home/alexander/vercors/min.java-4-26--4-33;unique_id=137)                                                          
        at viper.api.backend.SilverBackend.$anonfun$transform$1(SilverBackend.scala:107)                                                                                                                                                                        
        at hre.progress.task.NameSequenceTask.scope(NameSequenceTask.scala:16)                                                                                                                                                                                  
        at hre.progress.Progress$.stages(Progress.scala:47)                                                                                                                                                                                                     
        at viper.api.backend.SilverBackend.transform(SilverBackend.scala:90)                                                                                                                                                                                    
        at viper.api.backend.SilverBackend.transform$(SilverBackend.scala:81)                                                                                                                                                                                   
        at viper.api.backend.silicon.Silicon.transform(Silicon.scala:34)                                                                                                                                                                                        
        at vct.main.stages.SilverBackend.transform(Backend.scala:196)                                                                                                                                                                                           
        at vct.main.stages.Backend.$anonfun$run$3(Backend.scala:152)

I believe this is specifically because the type of write is TBoundedInt which can be coerced into TInt causing this to be treated as an integer division. Then once we get to Viper there's a mismatch because there write is of type Perm and the function truncdiv expects only Ints. Possible solutions:

• Make the type of write TFraction
• Generate an error when using the / operator on permission values instead of the \ operator

Also I think we should mention on the wiki somewhere that integer division and modulo is implemented differently in PVL versus our other frontends