Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [static-analysis]

The tag has no usage guidance.

1
vote
0answers
40 views

Small step vs big step semantics for static analysis?

To be an honest question poster I do not yet fully grasp the difference between small step and big step semantics. There was a good discussion here My question is if I were to do static analysis on ...
2
votes
1answer
18 views

Modelling regex replacement via a DFA

I wish to model the following common construction in code via a finite state automaton for the purposes of static analysis: ...
2
votes
0answers
21 views

Metrics for measuring and scoring automated “code analysis”?

I am writing various "program analysis" (aka static code analysis) algorithms. I am looking for ideas for metrics to measure how well my algorithms "understand the code". Some ideas i have so far : ...
0
votes
0answers
25 views

Sufficient conditions for an analysis using a monotone framework to converge

We define a monotone framework as follows: $\begin{align*} in(\ell) &=\begin{cases} \mathrm{Initial} & \text{when $\ell\in$ Entry Labels}\\\\ \bigoplus \{out(\ell') \mid (\ell',\ell) \in \...
0
votes
0answers
36 views

Optimize Algorithm For Shut in Box Game

This game is a simplified version of Shut the Box. There are 9 tiles (1,2,3,4,5...9). The initial tiles are unflipped. You have 2 dices. Each round, the player rolls the 2 dices and their sum is S. ...
2
votes
2answers
31 views

When to use Context-(in)Sensitive Inter-procedural Data Flow Analysis

I've been exploring the differences between Context Sensitive Analysis (CSA) and Context Insensitive Analysis (CIA), members of ...
3
votes
0answers
43 views

Why LLVM is not suitable to design a static analyzer?

I'm reading a paper, and there is this paragraph about LLVM: ''it heavily relies on the static single assignment form (SSA) which cannot be readily used to design an abstract interpreter. The $\...
2
votes
0answers
29 views

What is synonym propagation?

I am currently reading SmartCheck: Static Analysis of Ethereum Smart Contracts (Tikhomirov et al., WETSEB'18; PDF). In section 3.1 it talks briefly about synonym propagation. What is synonym ...
2
votes
1answer
143 views

What is a hyper property?

I am reading the paper Foundations and tools for the static analysis of Ethereum contracts, by Grischenko et al. Sometimes the authors speak about hyper properties (e.g. Section 5). What exactly is a ...
2
votes
0answers
58 views

Is there a language-independent, static analysis framework?

I'm looking for a generic static analysis framework that could be used to detect problems that aren't necessarily specific to a particular programming language; for example: Variable taint checking / ...
2
votes
0answers
31 views

State-of-the-art for Set Constraints?

I've recently stumbled across the field of Set constraints for program analysis, that is, solving equations of the form $exp_1 \subseteq exp_2$, where (depending on the particular variant of the ...
0
votes
0answers
263 views

Pseudocode for constructing control flow graph

I'm trying to build a complexity analysis tool and I need an algorithm for constructing the control flow graph (to get cyclomatic and eventually essential complexity). I couldn't find any pseudocode ...
3
votes
2answers
67 views

What counts as automatic program analysis?

I'm trying to understand the definition of program analysis on Wikipedia: Program analysis is the process of automatically analyzing the behavior of computer programs regarding a property such as ...
2
votes
1answer
37 views

Cut costly functions in inter-procedural abstract interpretation

I am performing some inter-procedural abstract interpretation to capture certain program properties. Following the standard way, what I am doing is to maintain a work list of to-be-analyzed functions, ...
6
votes
1answer
131 views

Memory needed for computational graph

Suppose we have a set of equations like this p7=f(p1+p6); p6=f(p2+p5); p5=f(p3+p4); p4=f(p3); p3=f(p2); p2=f(p1); p1=f() It can be represented by computational ...
1
vote
1answer
52 views

Data flow equations to determine value dependencies

I need to define the data-flow analysis equations to determine the value dependencies of an statement. For example: a = 9 b = a + 7 c = b * 2 the value of <...
24
votes
4answers
4k views

Is the halting problem decidable for pure programs on an ideal computer?

It's fairly simple to understand why the halting problem is undecidable for impure programs (i.e., ones that have I/O and/or states dependent on the machine-global state); but intuitively, it seems ...
2
votes
2answers
177 views

“taintedness” vs. “taintness”

In the context of information flow, when you talk about the property of variables being tainted, do you speak about "taintness" or "taintedness"? Both occur online, both sound weird to me. An example ...
2
votes
1answer
58 views

What does “post-image analysis” mean in the context of formal program analysis?

I am reviewing an anonymous paper about a sort of static analysis of programs that uses the phrase "post-image analysis", or "post-image operation" without defining what that is. I am guessing it is a ...
1
vote
1answer
168 views

Calculating attributes' values in the semantic analysis stage

I'm reading through the book : "Compiler Construction: Principles and Practice". In chapter 6 : semantic analysis, an example about attribute grammars is given. The example is of a simple integer ...
1
vote
1answer
90 views

Recognizing primitive recursion

I am trying to write a program to recognize if a given lambda calculus expression is primitive recursive. I believe that a general algorithm to do this does not exist, but I am interested in the most ...
0
votes
1answer
33 views

Is it “valid” for semantic functions to query outside of the grammar in attribute grammars?

Is it valid (in the sense of formal grammars or formal language theory) to refer to outside of the grammar in attribute grammars? What I mean is that since attribute grammars can contain semantic ...
3
votes
1answer
346 views

How to build a label flow graph for static analysis

I'm new to world of static analysis and am trying to build a new analysis of C programs for llvm compiler. I've started with the build of the graph of the constraints of the program: The edges ...