Data Range Specification file - how to force Code Prover to use the right one?

For context, I'm working on a project to try and reduce the number of orange checks in our runs of Code Prover. The idea is that I have a Python script automatically edit a DRS file and patch as many variables and pointers as possible with a valid INIT range, and hopefully reduce the thousands of orange checks to a more manageable number.

I'm having some difficulty making sure Code Prover uses the right constraints file though. The launching command uses an Options text file that includes the line:

-data-range-specifications [path to my file]

The program seems to ignore this file and arbitrarily pick a different one though (most recently, it picked a file that I had recently altered manually through the Code Prover GUI, even though I had renamed that file and moved it to a different directory).

There are a number of warnings in the log from parsing the DRS file, but no errors (and I don't think they're related to my modifications). Is it possible those are making it choose a different file?

Is there something else I can do to control which DRS file is used?

Answer 1

[Alexandre De Barros]

Hello Jeff,

from what I read, everything seems correct in terms of options. It is then strange that the program seems to ignore your DRS file.

I suggest you to contact the technical support, and attach a verification log file, the launching script and the DRS file.

Regards, Alexandre

[Jeff Campbell]

Thanks Alexandre, I'll do that. I should also note that after posting this question I found that if I make sure the DRS file is the only one of its kind in the local directory and subdirectories, then Code Prover chooses it correctly.