Improved Loop Execution Modeling in the Clang Static Analyzer

The LLVM Clang Static Analyzer is a source code analysis tool which aims to find bugs in C, C++, and Objective-C programs using symbolic execution, i.e. it simulates the possible execution paths of the code. Currently the simulation of the loops is somewhat naive (but efficient), unrolling the loops a predefined constant number of times. However, this approach can result in a loss of coverage in various cases. This study aims to introduce two alternative approaches which can extend the current method and can be applied simultaneously: (1) determining loops worth to fully unroll with applied heuristics, and (2) using a widening mechanism to simulate an arbitrary number of iteration steps. These methods were evaluated on numerous open source projects, and proved to increase coverage in most of the cases. This work also laid the infrastructure for future loop modeling improvements.

Download Full-text

Map2Check: Using Symbolic Execution and Fuzzing

Tools and Algorithms for the Construction and Analysis of Systems - Lecture Notes in Computer Science ◽

10.1007/978-3-030-45237-7_29 ◽

2020 ◽

pp. 403-407 ◽

Cited By ~ 1

Author(s):

Herbert Rocha ◽

Rafael Menezes ◽

Lucas C. Cordeiro ◽

Raimundo Barreto

Keyword(s):

Software Verification ◽

Symbolic Execution ◽

Source Code ◽

Reachability Analysis ◽

Experimental Results ◽

Safety Properties ◽

C Programs ◽

Verification Tool ◽

Inductive Invariants ◽

Monitor Data

Abstract Map2Check is a software verification tool that combines fuzzing, symbolic execution, and inductive invariants. It automatically checks safety properties in C programs by adopting source code instrumentation to monitor data (e.g., memory pointers) from the program’s executions using LLVM compiler infrastructure. For SV-COMP 2020, we extended Map2Check to exploit an iterative deepening approach using LibFuzzer and Klee to check for safety properties. We also use Crab-LLVM to infer program invariants based on reachability analysis. Experimental results show that Map2Check can handle a wide variety of safety properties in several intricate verification tasks from SV-COMP 2020.

Download Full-text

The source code analysis tool construction project

Proceedings of the conference on TRI-Ada '97 - TRI-Ada '97 ◽

10.1145/269629.269645 ◽

1997 ◽

Cited By ~ 1

Author(s):

Richard Conn

Keyword(s):

Source Code ◽

Construction Project ◽

Analysis Tool ◽

Source Code Analysis ◽

Code Analysis

Download Full-text

An automated memory error detection technique using source code analysis in C programs

The KIPS Transactions PartD ◽

10.3745/kipstd.2007.14-d.6.675 ◽

2007 ◽

Vol 14D (6) ◽

pp. 675-688 ◽

Cited By ~ 1

Author(s):

Dae-Wan Cho ◽

Seung-Uk Oh ◽

Hyeon-Soo Kim

Keyword(s):

Error Detection ◽

Source Code ◽

Detection Technique ◽

Source Code Analysis ◽

Code Analysis ◽

Memory Error ◽

C Programs

Download Full-text

Using unreachable code analysis in static analysis tool for finding defects in source code

Proceedings of the Institute for System Programming of RAS ◽

10.15514/ispras-2016-28(5)-9 ◽

2016 ◽

Vol 28 (5) ◽

pp. 145-158

Author(s):

R.R. Mulyukov ◽

A.E. Borodin

Keyword(s):

Static Analysis ◽

Source Code ◽

Analysis Tool ◽

Code Analysis ◽

Static Analysis Tool

Download Full-text

Enhanced Bug Prediction in JavaScript Programs with Hybrid Call-Graph Based Invocation Metrics

Technologies ◽

10.3390/technologies9010003 ◽

2020 ◽

Vol 9 (1) ◽

pp. 3

Author(s):

Gábor Antal ◽

Zoltán Tóth ◽

Péter Hegedűs ◽

Rudolf Ferenc

Keyword(s):

Software Maintenance ◽

Positive Impact ◽

Source Code ◽

Code Analysis ◽

Static Source ◽

Static Code Analysis ◽

Function Calls ◽

Hybrid Code ◽

Code Metrics ◽

Scripting Language

Bug prediction aims at finding source code elements in a software system that are likely to contain defects. Being aware of the most error-prone parts of the program, one can efficiently allocate the limited amount of testing and code review resources. Therefore, bug prediction can support software maintenance and evolution to a great extent. In this paper, we propose a function level JavaScript bug prediction model based on static source code metrics with the addition of a hybrid (static and dynamic) code analysis based metric of the number of incoming and outgoing function calls (HNII and HNOI). Our motivation for this is that JavaScript is a highly dynamic scripting language for which static code analysis might be very imprecise; therefore, using a purely static source code features for bug prediction might not be enough. Based on a study where we extracted 824 buggy and 1943 non-buggy functions from the publicly available BugsJS dataset for the ESLint JavaScript project, we can confirm the positive impact of hybrid code metrics on the prediction performance of the ML models. Depending on the ML algorithm, applied hyper-parameters, and target measures we consider, hybrid invocation metrics bring a 2–10% increase in model performances (i.e., precision, recall, F-measure). Interestingly, replacing static NOI and NII metrics with their hybrid counterparts HNOI and HNII in itself improves model performances; however, using them all together yields the best results.

Download Full-text

Fifth IEEE International Workshop on Source Code Analysis and Manipulation - Copyright

Fifth IEEE International Workshop on Source Code Analysis and Manipulation (SCAM'05) ◽

10.1109/scam.2005.10 ◽

2005 ◽

Keyword(s):

International Workshop ◽

Source Code ◽

Source Code Analysis ◽

Code Analysis ◽

Ieee International Workshop

Download Full-text

Introduction to Special Issue on Source Code Analysis and Manipulation

Journal of Systems and Software ◽

10.1016/j.jss.2021.110949 ◽

2021 ◽

pp. 110949

Author(s):

Yoshiki Higo ◽

Alexander Serebrenik

Keyword(s):

Source Code ◽

Special Issue ◽

Source Code Analysis ◽

Code Analysis

Download Full-text

Source Code Analysis of a Connection-Oriented File Reader Server Socket Program in Java and Removal of the Security Vulnerabilities

Lecture Notes in Electrical Engineering - Computer Networks & Communications (NetCom) ◽

10.1007/978-1-4614-6154-8_61 ◽

2013 ◽

pp. 621-629

Author(s):

N. Meghanathan

Keyword(s):

Source Code ◽

Security Vulnerabilities ◽

Source Code Analysis ◽

Code Analysis

Download Full-text

FuSeBMC: A White-Box Fuzzer for Finding Security Vulnerabilities in C Programs (Competition Contribution)

Fundamental Approaches to Software Engineering - Lecture Notes in Computer Science ◽

10.1007/978-3-030-71500-7_19 ◽

2021 ◽

pp. 363-367 ◽

Cited By ~ 1

Author(s):

Kaled M. Alshmrany ◽

Rafael S. Menezes ◽

Mikhail R. Gadelha ◽

Lucas C. Cordeiro

Keyword(s):

Model Checking ◽

Symbolic Execution ◽

Bounded Model Checking ◽

Test Cases ◽

Security Vulnerabilities ◽

C Programs ◽

Code Coverage

AbstractWe describe and evaluate a novel white-box fuzzer for C programs named , which combines fuzzing and symbolic execution, and applies Bounded Model Checking (BMC) to find security vulnerabilities in C programs. explores and analyzes C programs (1) to find execution paths that lead to property violations and (2) to incrementally inject labels to guide the fuzzer and the BMC engine to produce test-cases for code coverage. successfully participates in Test-Comp’21 and achieves first place in the category and second place in the category.

Download Full-text