Databases
StackOverflow2013
Postsdbo
PO
 

Note that there are some explanatory texts on larger screens.

plurals
  1. PO
    primarykey
    data
    text
    <p>You can express your assertion as a property to check with a static analyzer and let the analyzer do the check. This has some of the properties of what you want to do:</p> <ul> <li><p>the property is written in the source code,</p></li> <li><p>it doesn't pollute the generated binary code.</p></li> </ul> <p>However, it is different from a compile-time assertion because it needs a separate tool to be run on the program for checking. And perhaps it's a sanity check on the compiler you were trying to do, in which case this doesn't help because the static analyzer doesn't check what the compiler does, only what it <em>should</em> do. ADDED: if it's for QA, then writing "formal" assertions that can be verified statically is all the rage nowadays. The approach below is very similar to .NET contracts that you may have heard about, but it is for C.</p> <ul> <li><p>You may not think much of static analyzers, but it is loops and function calls that cause them to become imprecise. It's easier for them to get a clear picture of what is going on at initialization time, before any of these have happened.</p></li> <li><p>Some analyzers advertise themselves as "correct", that is, they do not remain silent if the property you write is outside of their capabilities. In this case they complain that they can't prove it. If this happens, after you have convinced yourself that the problem is with the analyzer and not with your array, you'll be left where you are now, looking for another way.</p></li> </ul> <p>Taking the example of the analyzer I am familiar with:</p> <pre><code>const int t[3] = {1, 2, 3}; int x; int main(){ //@ assert t[2] == 3 ; /* more code doing stuff */ } </code></pre> <p>Run the analyzer:</p> <pre><code>$ frama-c -val t.i ... t.i:7: Warning: Assertion got status valid. Values of globals at initialization t[0] ∈ {1; } [1] ∈ {2; } [2] ∈ {3; } x ∈ {0; } ... </code></pre> <p>In the logs of the analyzer, you get:</p> <ul> <li>its version of what it thinks the initial values of globals are,</li> <li>and its interpretation of the assertion you wrote in the //@ comment. Here it goes through the assertion a single time and finds it valid.</li> </ul> <p>People who use this kind of tool build scripts to extract the information they're interested in from the logs automatically. However, as a negative note, I have to point out that if you are afraid a test could eventually be forgotten, you should also worry about the mandatory static analyzer pass being forgotten after code modifications.</p>
    singulars
    1. This table or related slice is empty.
    1. POC Compile-Time assert with constant array
      singulars
      1. PTQuestion
    1. PTAnswer
    1. This table or related slice is empty.
    1. USPascal Cuoq
    plurals
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. COThanks. I'll look more into it, but I feel it's a bit overkill for my purposes as I only need to verify 2 arrays and the frama-c is a 150MB compressed program.
      singulars
      1. PO
      1. USEldad
 

Querying!

 
Guidance
A row detail

Detail views are divided into sections. All the information in the data section comes from columns in the selected row. The other sections display data from other, related rows.

Related data can be related in a to-one or a to-many fashion. Captions of data related in a to-many fashion link to a list view showing a filtered view of the table.

Try moving around until you find a non-empty to-many entry and click on the label to get to one. You can move back to the root by clicking on the database name in the header.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload