pith. sign in

arxiv: 2605.27531 · v1 · pith:YMXBWOUCnew · submitted 2026-05-26 · 💻 cs.PL · cs.CL· cs.SE

Agentic Separation Logic Specification Synthesis

Tarun Suresh , David Korczynski , Julien Vanegue This is my paper

Pith reviewed 2026-06-29 14:09 UTC · model grok-4.3

classification 💻 cs.PL cs.CLcs.SE
keywords specification synthesisseparation logicagentic systemsC++ verificationcounterexample-guided refinementheap tracingformal specifications
0
0 comments X

The pith

Spec-Agent synthesizes valid specifications for 85% of functions in large C++ codebases by selecting from a ladder of separation logics and refining via counterexample feedback.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents Spec-Agent as a method to automatically infer formal specifications from C++ program implementations. It addresses the challenge of scaling to large repositories while handling features like dynamic memory and heap structures by using a progression of specification languages. The system selects the appropriate language level through static analysis and runtime tracing, converts tests into fuzz harnesses, and iteratively improves LLM-generated candidates with counterexample guidance. A sympathetic reader would care because this could reduce the manual effort required for verification, refactoring, and optimization in systems code.

Core claim

Spec-Agent targets propositional logic, first-order logic, propositional separation logic, and first-order separation logic. For each function it applies static analysis and runtime heap tracing to pick the target language, generalizes functional tests into fuzz harnesses, and refines LLM candidates through counterexample-guided feedback. On open-source C++ codebases with millions of lines, it produces valid specifications for 85% of target functions with no false positives under fuzzing and expert validation, at 10x lower token cost than Claude Code Opus 4.6.

What carries the argument

Spec-Agent, an agentic system that selects a target specification language from a ladder (propositional logic to first-order separation logic) using static analysis and runtime heap tracing, then applies counterexample-guided LLM refinement on fuzz-harness feedback.

Load-bearing premise

Static analysis plus runtime heap tracing can reliably pick the right specification language level and the counterexample-guided refinement loop will converge to correct specifications without systematically missing complex aliasing or ownership patterns.

What would settle it

A C++ function in a large codebase where Spec-Agent outputs a specification that passes fuzzing and initial expert review but later fails to capture an aliasing or ownership relation that causes a verification tool to reject a correct program or accept an incorrect one.

Figures

Figures reproduced from arXiv: 2605.27531 by David Korczynski, Julien Vanegue, Tarun Suresh.

Figure 1
Figure 1. Figure 1: Specification validity and cost comparison of Spec-Agent versus Claude Code. [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Left: A memory-manipulating program with separation logic annotations. Right: A function [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Program specification languages supported by Spec-Agent. [PITH_FULL_IMAGE:figures/full_fig_p003_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Inside Spec-Agent: Automated fuzz-guided refinement of candidate specifications. The [PITH_FULL_IMAGE:figures/full_fig_p004_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: The specification lattice: Spec-Agent maintains an order-theoretic lattice of specification [PITH_FULL_IMAGE:figures/full_fig_p005_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Number of BDE functions with correctly synthesized specifications by number of refinement [PITH_FULL_IMAGE:figures/full_fig_p007_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Distribution of cumulative inference and testing time for each BDE function with an [PITH_FULL_IMAGE:figures/full_fig_p008_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Coverage distributions for Spec-Agent’s LLM-generated fuzz harnesses on BDE and BMQ. [PITH_FULL_IMAGE:figures/full_fig_p013_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Distribution of lines of code per function for the evaluated functions in BDE (left) and [PITH_FULL_IMAGE:figures/full_fig_p013_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: First-order logic contract capturing a loop invariant directly in the postcondition (ensures), [PITH_FULL_IMAGE:figures/full_fig_p015_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: A first-order separation logic contract capturing deep memory constraints between C++ [PITH_FULL_IMAGE:figures/full_fig_p015_11.png] view at source ↗
read the original abstract

Specification synthesis, the task of automatically inferring formal specifications from program implementations and natural language, is important for refactoring, transpilation, optimization, and verification, yet remains an open challenge for large C++ repositories. Existing LLM-based approaches fail to simultaneously scale to such repositories, produce specifications expressive enough to capture systems-code features such as dynamic memory and heap-allocated data structures, and systematically validate those specifications to rule out incorrect candidates. We present Spec-Agent, an agentic system for synthesizing expressive, well-validated specifications across large C++ codebases. Spec-Agent targets a ladder of specification languages: propositional logic, first-order logic, propositional separation logic, and first-order separation logic. For each function, Spec-Agent uses static analysis and runtime heap tracing to select the appropriate target specification language, generalizes existing functional tests into fuzz harnesses, and iteratively refines LLM-generated candidates via counterexample-guided feedback. We evaluate Spec-Agent on open source C++ codebases comprising millions of lines of code. Spec-Agent synthesizes valid specifications for 85% of target functions, with no false positives observed under fuzzing and expert validation, outperforming Claude Code Opus 4.6 at 10x lower token cost.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The manuscript presents Spec-Agent, an agentic system for synthesizing specifications across a ladder of languages (propositional logic, first-order logic, propositional separation logic, first-order separation logic) for functions in large C++ codebases. For each function it applies static analysis plus runtime heap tracing to select the target language, generalizes existing tests into fuzz harnesses, and performs counterexample-guided LLM refinement. Evaluation on open-source C++ repositories comprising millions of lines of code reports that Spec-Agent produces valid specifications for 85% of target functions with zero false positives under fuzzing and expert validation, at 10x lower token cost than Claude Code Opus 4.6.

Significance. If the evaluation holds, the result would be significant for automated specification synthesis in systems code, demonstrating a scalable combination of static analysis, dynamic tracing, and LLM refinement that handles heap-allocated structures. The explicit language ladder and the use of external open-source repositories for evaluation are strengths that support reproducibility.

major comments (2)
  1. [§5 Evaluation] §5 Evaluation, results paragraph: the 85% validity rate with zero false positives is load-bearing for the central claim, yet the manuscript provides no quantitative breakdown of success rate by specification language level, no description of how target functions were sampled from the repositories, and no coverage metrics (e.g., branch or alias coverage) for the generated fuzz harnesses.
  2. [§3.3 and §4.1] §3.3 Refinement loop and §4.1 Language selection: the claim that counterexample-guided refinement plus static+dynamic selection reliably produces complete specs is undermined by the absence of any experiment or argument showing that the fuzz harnesses (derived from existing tests) exercise aliasing, ownership transfer, or deep heap invariants; without such evidence the zero-false-positive result may reflect coverage gaps rather than specification correctness.
minor comments (2)
  1. [Abstract] The abstract states the token-cost comparison but does not specify the exact token counts or the prompting setup used for the Claude baseline; this should be added for reproducibility.
  2. [§2] Notation for the four specification languages is introduced without a compact summary table; a small table in §2 would improve readability.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the detailed and constructive comments. We address each major comment below, indicating planned revisions where appropriate.

read point-by-point responses

  1. Referee: [§5 Evaluation] §5 Evaluation, results paragraph: the 85% validity rate with zero false positives is load-bearing for the central claim, yet the manuscript provides no quantitative breakdown of success rate by specification language level, no description of how target functions were sampled from the repositories, and no coverage metrics (e.g., branch or alias coverage) for the generated fuzz harnesses.

    Authors: We agree that a per-language breakdown would strengthen the presentation and will add a table in the revised §5 reporting success rates separately for propositional logic, first-order logic, propositional separation logic, and first-order separation logic. Target functions were selected as every function possessing at least one existing unit test in the chosen open-source repositories; we will explicitly state this sampling criterion. The manuscript does not report branch or alias coverage for the derived fuzz harnesses, because validation was performed via observed fuzz outcomes plus expert review rather than coverage instrumentation. We will add a short limitations paragraph acknowledging the absence of these metrics. revision: partial

  2. Referee: [§3.3 and §4.1] §3.3 Refinement loop and §4.1 Language selection: the claim that counterexample-guided refinement plus static+dynamic selection reliably produces complete specs is undermined by the absence of any experiment or argument showing that the fuzz harnesses (derived from existing tests) exercise aliasing, ownership transfer, or deep heap invariants; without such evidence the zero-false-positive result may reflect coverage gaps rather than specification correctness.

    Authors: Section 4.1 selects the specification language by combining static analysis (to detect heap allocation and pointer usage) with runtime heap tracing; this choice is intended to match the required expressiveness rather than to guarantee completeness. The refinement loop in §3.3 feeds counterexamples discovered by the fuzz harnesses back to the LLM. We do not claim that the resulting specifications are complete for all possible executions; the zero false-positive result is reported only under the inputs exercised by the fuzz harnesses and under expert validation. We will revise the text in §3.3 to make this scope explicit and to note that the harnesses inherit the coverage of the original tests. revision: yes

Circularity Check

0 steps flagged

No circularity; empirical system evaluated on external codebases with no fitted predictions or self-referential derivations

full rationale

The paper presents an engineering system (Spec-Agent) that selects spec languages via static analysis and runtime tracing, generates fuzz harnesses from existing tests, and refines LLM outputs via counterexample feedback. No equations, parameters, or first-principles derivations are described. The 85% validity claim rests on evaluation against external open-source C++ repositories (millions of LOC) plus fuzzing and expert validation, not on any quantity fitted to the target data and then re-predicted. No self-citations, uniqueness theorems, or ansatzes appear in the abstract or described methodology. The derivation chain is therefore self-contained and externally falsifiable.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Abstract-only review yields no explicit free parameters, ad-hoc axioms, or invented entities; the approach relies on standard separation-logic semantics and LLM prompting whose details are not supplied.

axioms (1)
  • domain assumption Separation logic correctly models heap ownership and aliasing in C++
    Invoked when targeting first-order separation logic for heap-allocated structures.

pith-pipeline@v0.9.1-grok · 5741 in / 1267 out tokens · 29800 ms · 2026-06-29T14:09:58.800803+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

137 extracted references · 2 canonical work pages · 1 internal anchor

  1. [1]

    Claude code: Command line tool for agentic coding, 2024

    Anthropic. Claude code: Command line tool for agentic coding, 2024

    2024

  2. [2]

    https://github.com/bloomberg/bde

    BDE. https://github.com/bloomberg/bde

  3. [3]

    A modern, high-performance message queue

    BlazingMQ. A modern, high-performance message queue

  4. [4]

    Compositional shape analysis by means of bi-abduction

    Cristiano Calcagno, Dino Distefano, Peter O’Hearn, and Hongseok Yang. Compositional shape analysis by means of bi-abduction. InProceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 289–300, 2009

    2009

  5. [5]

    clang: a C language family frontend for LLVM

    Clang. clang: a C language family frontend for LLVM

  6. [6]

    Frama-c: A software analysis perspective

    Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. Frama-c: A software analysis perspective. InInternational conference on software engineering and formal methods, pages 233–247. Springer, 2012

    2012

  7. [7]

    Madeline Endres, Sarah Fakhoury, Saikat Chakraborty, and Shuvendu K. Lahiri. Can large language models transform natural language intent into formal method postconditions?Proc. ACM Softw. Eng., 1(FSE):1889–1912, 2024

    1912

  8. [8]

    Ernst, Jeff H

    Michael D. Ernst, Jeff H. Perkins, Philip J. Guo, Stephen McCamant, Carlos Pacheco, Matthew S. Tschantz, and Chen Xiao. The daikon system for dynamic detection of likely invariants.Sci. Comput. Program., 69(1-3):35–45, 2007

    2007

  9. [9]

    Static verification for code contracts

    Manuel Fähndrich. Static verification for code contracts. InInternational Static Analysis Symposium, pages 2–5. Springer, 2010

    2010

  10. [10]

    Assigning meanings to programs

    Robert W Floyd. Assigning meanings to programs. InProgram Verification: Fundamental Issues in Computer Science, pages 65–81. Springer, 1993

    1993

  11. [11]

    Security weaknesses of copilot-generated code in github projects: An empirical study, 2025

    Yujia Fu, Peng Liang, Amjed Tahir, Zengyang Li, Mojtaba Shahin, Jiaxin Yu, and Jinfu Chen. Security weaknesses of copilot-generated code in github projects: An empirical study, 2025

    2025

  12. [12]

    An axiomatic basis for computer programming.Communica- tions of the ACM, 12(10):576–580, 1969

    Charles Antony Richard Hoare. An axiomatic basis for computer programming.Communica- tions of the ACM, 12(10):576–580, 1969

    1969

  13. [13]

    Jimenez, John Yang, Alexander Wettig, Shunyu Yao, Kexin Pei, Ofir Press, and Karthik Narasimhan

    Carlos E. Jimenez, John Yang, Alexander Wettig, Shunyu Yao, Kexin Pei, Ofir Press, and Karthik Narasimhan. Swe-bench: Can language models resolve real-world github issues?, 2024

    2024

  14. [14]

    Gonzalez, Hao Zhang, and Ion Stoica

    Woosuk Kwon, Zhuohan Li, Siyuan Zhuang, Ying Sheng, Lianmin Zheng, Cody Hao Yu, Joseph E. Gonzalez, Hao Zhang, and Ion Stoica. Efficient memory management for large lan- guage model serving with pagedattention. InProceedings of the ACM SIGOPS 29th Symposium on Operating Systems Principles, 2023

    2023

  15. [15]

    SLING: using dynamic analysis to infer program invariants in separation logic

    Ton Chanh Le, Guolong Zheng, and ThanhVu Nguyen. SLING: using dynamic analysis to infer program invariants in separation logic. In Kathryn S. McKinley and Kathleen Fisher, editors, Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 2019, pages 788–801. ACM, 2019

    2019

  16. [16]

    Towards general loop invariant generation: A benchmark of programs with memory manipulation

    Chang Liu, Xiwei Wu, Yuan Feng, Qinxiang Cao, and Junchi Yan. Towards general loop invariant generation: A benchmark of programs with memory manipulation. In Amir Globersons, Lester Mackey, Danielle Belgrave, Angela Fan, Ulrich Paquet, Jakub M. Tomczak, and Cheng Zhang, editors,Advances in Neural Information Processing Systems 38: Annual Conference on Neu...

    2024

  17. [17]

    Is your code generated by chatGPT really correct? rigorous evaluation of large language models for code generation

    Jiawei Liu, Chunqiu Steven Xia, Yuyao Wang, and LINGMING ZHANG. Is your code generated by chatGPT really correct? rigorous evaluation of large language models for code generation. InThirty-seventh Conference on Neural Information Processing Systems, 2023

    2023

  18. [18]

    Specgen: Automated generation of formal program specifications via large language models

    Lezhi Ma, Shangqing Liu, Yi Li, Xiaofei Xie, and Lei Bu. Specgen: Automated generation of formal program specifications via large language models. In47th IEEE/ACM International Conference on Software Engineering, ICSE 2025, Ottawa, ON, Canada, April 26 - May 6, 2025, pages 16–28. IEEE, 2025. 10

    2025

  19. [19]

    An empirical study of the reliability of unix utilities.Commun

    Barton Miller, Lars Fredriksen, and Bryan So. An empirical study of the reliability of unix utilities.Commun. ACM, 33:32–44, 12 1990

    1990

  20. [20]

    Separation logic.Communications of the ACM, 62(2):86–95, 2019

    Peter O’Hearn. Separation logic.Communications of the ACM, 62(2):86–95, 2019

    2019

  21. [21]

    Qwen3-coder-next technical report

    Qwen Team. Qwen3-coder-next technical report. Technical report. Accessed: 2026-02-03

    2026

  22. [22]

    Qwen3.5: Towards native multimodal agents, February 2026

    Qwen Team. Qwen3.5: Towards native multimodal agents, February 2026

    2026

  23. [23]

    Ad- dresssanitizer: A fast address sanity checker

    Konstantin Serebryany, Derek Bruening, Alexander Potapenko, and Dmitriy Vyukov. Ad- dresssanitizer: A fast address sanity checker. In Gernot Heiser and Wilson C. Hsieh, editors, Proceedings of the 2012 USENIX Annual Technical Conference, USENIX ATC 2012, Boston, MA, USA, June 13-15, 2012, pages 309–318. USENIX Association, 2012

    2012

  24. [24]

    Continuous fuzzing with libfuzzer and addresssanitizer

    Kosta Serebryany. Continuous fuzzing with libfuzzer and addresssanitizer. In2016 IEEE Cybersecurity Development (SecDev), pages 157–157, 2016

    2016

  25. [25]

    LLMs versus the Halting Problem: Characterizing Program Termination Reasoning

    Oren Sultan, Jordi Armengol-Estape, Pascal Kesseli, Julien Vanegue, Dafna Shahaf, Yossi Adi, and Peter O’Hearn. Llms versus the halting problem: Revisiting program termination prediction. arXiv preprint arXiv:2601.18987, 2026

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  26. [26]

    Barrett, David L

    Chuyue Sun, Viraj Agashe, Saikat Chakraborty, Jubi Taneja, Clark W. Barrett, David L. Dill, Xiaokang Qiu, and Shuvendu K. Lahiri. Classinvgen: Class invariant synthesis using large language models. In Mirco Giacobbe and Anna Lukina, editors,AI Verification - Second International Symposium, SAIV 2025, Zagreb, Croatia, July 21-22, 2025, Proceedings, Lecture...

    2025

  27. [27]

    FAIR CodeGen team, Jade Copet, Quentin Carbonneaux, Gal Cohen, Jonas Gehring, Jacob Kahn, Jannik Kossen, Felix Kreuk, Emily McMilin, Michel Meyer, Yuxiang Wei, David Zhang, Kunhao Zheng, Jordi Armengol-Estapé, Pedram Bashiri, Maximilian Beck, Pierre Chambon, Abhishek Charnalia, Chris Cummins, Juliette Decugis, Zacharias V . Fisches, François Fleuret, Fabi...

    2025

  28. [28]

    Qwen2.5: A party of foundation models, September 2024

    Qwen Team. Qwen2.5: A party of foundation models, September 2024

    2024

  29. [29]

    Together ai pricing, 2026

    Together AI. Together ai pricing, 2026

    2026

  30. [30]

    An incremental parsing system for programming tools

    Tree-sitter. An incremental parsing system for programming tools

  31. [31]

    On computable numbers, with an application to the entschei- dungsproblem.J

    Alan Mathison Turing et al. On computable numbers, with an application to the entschei- dungsproblem.J. of Math, 58(345-363):5, 1936

    1936

  32. [32]

    Fun2spec: Code contract synthesis at scale

    Shubham Ugare, Tarun Suresh, Sasa Misailovic, and Julien Vanegue. Fun2spec: Code contract synthesis at scale. InCompanion Proceedings of the 34th ACM International Conference on the Foundations of Software Engineering (FSE Companion ’26), Industry Track, Montreal, QC, Canada, 2026. ACM

    2026

  33. [33]

    Towards practical reactive security audit using extended static checkers

    Julien Vanegue and Shuvendu K Lahiri. Towards practical reactive security audit using extended static checkers. In2013 IEEE Symposium on Security and Privacy, pages 33–47. IEEE, 2013

    2013

  34. [34]

    Shadows in the code: Exploring the risks and defenses of llm-based multi-agent software development systems, 2025

    Xiaoqing Wang, Keman Huang, Bin Liang, Hongyu Li, and Xiaoyong Du. Shadows in the code: Exploring the risks and defenses of llm-based multi-agent software development systems, 2025

    2025

  35. [35]

    Enchanting program specification synthesis by large language models using static analysis and program verification

    Cheng Wen, Jialun Cao, Jie Su, Zhiwu Xu, Shengchao Qin, Mengda He, Haokun Li, Shing-Chi Cheung, and Cong Tian. Enchanting program specification synthesis by large language models using static analysis and program verification. In Arie Gurfinkel and Vijay Ganesh, editors, Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, ...

    2024

  36. [36]

    Har- nessagent: Scaling automatic fuzzing harness construction with tool-augmented llm pipelines

    Kang Yang, Yunhang Zhang, Zichuan Li, Guanhong Tao, Jun Xu, and Xiaojing Liao. Har- nessagent: Scaling automatic fuzzing harness construction with tool-augmented llm pipelines. ArXiv, abs/2512.03420, 2025

    work page arXiv 2025

  37. [37]

    CISPA Helmholtz Center for Information Security, 2024

    Andreas Zeller, Rahul Gopinath, Marcel Böhme, Gordon Fraser, and Christian Holler.The Fuzzing Book. CISPA Helmholtz Center for Information Security, 2024. 12 A Additional Repository and Fuzzing Statistics This appendix includes a distributional supplement to the main evaluation showing the per-harness branch coverage of the generated fuzz harnesses. The X...

    2024

  38. [38]

    Filename:baljsn_encoder_testtypes.cpp,Function:EncoderTestChoiceWithAllCatego riesEnumeration::fromString,Logic: First Order Separation Logic, [code] requires:result != 0 && string != 0 && stringLength>= 0 ensures:(__out == 0 == > SEPEXISTS(0, 2, i, (stringLength == EncoderTestC hoiceWithAllCategoriesEnumeration::ENUMERATOR_INFO_ARRAY[i].d_ nameLength && ...

  39. [39]

    end(), it, EXISTS(__out.begin(), __out.end(), jt, *jt == *it)))

    Filename:ball_attributecontainerlist.cpp,Function:AttributeContainerList::operator=, Logic: First Order Separation Logic, [code] requires:SEPFORALL(rhs.begin(), rhs.end(), it, *it7→_) ensures:__out == *this && (__out == *this == > SEPFORALL(rhs.begin(), rhs. end(), it, EXISTS(__out.begin(), __out.end(), jt, *jt == *it)))

  40. [40]

    Filename:ball_log.cpp,Function:Log::format,Logic: First Order Separation Logic, [code] requires:format != 0 && buffer != 0 && SEPFORALL(0, numBytes, i, buffer + i 7→_) ensures:(__out == -1) || (__out != -1 && SEPFORALL(0, __out, i, buffer + i 7→ _ ))

  41. [41]

    Filename:ball_userfields.cpp,Function:UserFields::print,Logic: First Order Separa- tion Logic, [code] requires:true ensures:(stream.bad() == > __out == stream) && (stream.good() == > SEP- FORALL(0, length(), i, EXISTS(0, __out.size(), j, (__out + j)7→value(i))))

  42. [42]

    size() + 1 + j7→d_name_p[j]))

    Filename:balm_metricdescription.cpp,Function:MetricDescription::print,Logic: First Order Separation Logic, [code] 16 requires:true ensures:__out == stream && (SEPFORALL(0, d_category_p- >name().size(), i, stream + i 7→ d_category_p->name()[i]) ⋆ (stream + d_category_p->name().size() 7→ ’.’) ⋆ SEPFORALL(0, d_name_p.size(), j, stream + d_category_p- >name()...

  43. [43]

    INV ALID_ID

    Filename:balm_metricid.cpp,Function:MetricId::print,Logic: First Order Separation Logic, [code] requires:true ensures:(d_description_p == 0 == > SEPFORALL(0, strlen("INV ALID_ID"), i, stream + i 7→ "INV ALID_ID"[i])) && (d_description_p != 0 ==> SEPFORALL(0, strlen(*d_description_p), i, stream + i 7→ (*d_description_p)[i])) && (__out == stream)

  44. [44]

    Filename:balm_metricsample.cpp,Function:MetricSample::print,Logic: First Order Separation Logic, [code] requires:stream.good() && (spacesPerLevel>= 0) ensures:__out == stream && (stream.bad() || (stream.good() && SEPFORALL(0, strlen(NL), i, stream + i7→NL[i])))

  45. [45]

    Filename:balst_stacktraceprinter.cpp,Function:balst::operator <<,Logic: First Order Separation Logic, [code] requires:true ensures:__out == stream && (stream + 0 7→ bsl::endl ⋆ SEPFORALL(0, balst: :StackTracePrintUtil::printStackTrace(stream, object.d_maxFrames, object.d_dem anglingPreferredFlag, object.d_additionalIgnoreFrames + 1) - 1, i, stream + i + 1...

  46. [46]

    Filename:balst_stacktracetestallocator.cpp,Function:StackTraceTestAllocator::allocate, Logic: First Order Separation Logic, [code] requires:size>= 0 ensures:(size == 0 && __out == 0) || (size != 0 && __out != 0 && (__out 7→ _ ⋆ (__out - 1)7→_⋆SEPFORALL(0, d_traceBufferLength, i, (__out - 1 - i)7→_)))

  47. [47]

    Filename:balst_stacktraceutil.cpp,Function:findBasename,Logic: Propositional Logic, [code] requires:pathName != nullptr && strlen(pathName)>0 ensures:(__out >= pathName) && (__out == pathName || (*(__out - 1) == ’/’|| *(__out - 1) == ’\\’))

  48. [48]

    descriptor() == descriptor)) && (res_tmp == false ==> SEPFORALL(0, transitions

    Filename:baltzo_zoneinfo.cpp,Function:containsDescriptor,Logic: First Order Sepa- ration Logic, [code] requires:(res_tmp == true ==>SEPEXISTS(0, transitions.size(), i, transitions[i]. descriptor() == descriptor)) && (res_tmp == false ==> SEPFORALL(0, transitions. size(), i, transitions[i].descriptor() != descriptor)) ensures:(__out == true == > SEPEXISTS(...

  49. [49]

    Filename:baltzo_zoneinfobinaryreader.cpp,Function:areAllPrintable,Logic: First Order Separation Logic, [code] requires:buffer != 0 && length >= 0 && SEPFORALL(0, length, i, (buffer + i 7→ _)) ensures:(__out == true == > SEPFORALL(0, length, i, (buffer + i 7→ sep_v) && bdlb::CharType::isPrint(sep_v))) && (__out == false ==> SEPEXISTS(0, length, i, (buffer ...

  50. [50]

    first != prefix)) && (__out == lookupPredefinedPrefix(prefix).d_nsid))

    Filename:balxml_prefixstack.cpp,Function:PrefixStack::lookupNamespaceId,Logic: First Order Separation Logic, [code] requires:true ensures:(SEPEXISTS(0, d_numPrefixes, i, (d_prefixes[i].first == prefix) && (__ out == d_prefixes[i].second))) || (SEPFORALL(0, d_numPrefixes, i, (d_prefixes[i]. first != prefix)) && (__out == lookupPredefinedPrefix(prefix).d_nsid))

  51. [51]

    Filename:balxml_typesparserutil.cpp,Function:parseUnsignedInt,Logic: First Order Separation Logic, [code] requires:inputLength > 0 && SEPFORALL(0, inputLength, i, (input + i 7→ _ && input[i]>= ’0’ && input[i]<= ’9’)) ensures:(__out == BAEXML_SUCCESS)||(__out == BAEXML_FAILURE)

  52. [52]

    good() ensures:(__out == 0 ==>stream.good()) && (__out != 0 ==>stream.bad())

    Filename:balxml_typesprintutil.cpp,Function:printTextReplacingXMLEscapes,Logic: First Order Separation Logic, [code] requires:(dataLength >= 0 && SEPFORALL(0, dataLength, i, (data + i) 7→ _)) || (dataLength == -1 && SEPEXISTS(0, strlen(data), i, (data + i) 7→ _)) && stream. good() ensures:(__out == 0 ==>stream.good()) && (__out != 0 ==>stream.bad())

  53. [53]

    Filename:bbldc_daycountconvention.cpp,Function:DayCountConvention::print,Logic: First Order Separation Logic, [code] requires:true ensures:__out == stream && (SEPFORALL(0, strlen(toAscii(value)), i, (stream + i)7→toAscii(value)[i]))

  54. [54]

    Filename:bdlb_bitstringutil.cpp,Function:indent,Logic: First Order Separation Logic, [code] requires:level>= 0 && spacesPerLevel != 0 ensures:__out == stream && SEPFORALL(0, level * spacesPerLevel, i, (stream + i7→’ ’))

  55. [55]

    Filename:bdlb_string.cpp,Function:String::areEqualCaseless,Logic: First Order Separation Logic, [code] 18 requires:lhsString != nullptr && rhsString != nullptr && SEPFORALL(0, strlen(lhsString), i, (lhsString + i 7→ _)) && SEPFORALL(0, strlen(rhsString), i, (rhsString + i7→_)) ensures:(__out == true == > SEPFORALL(0, strlen(lhsString), i, (bdlb:: CharType...

  56. [56]

    get()[i])⋆stream.flushed())

    Filename:bdlbb_blob.cpp,Function:BlobBuffer::print,Logic: First Order Separation Logic, [code] requires:stream.good() ensures:__out == stream && (SEPFORALL(0, d_size, i, stream + i 7→ d_buffer. get()[i])⋆stream.flushed())

  57. [57]

    size(), i, d_unusedStack[i] != index))

    Filename:bdlc_indexclerk.cpp,Function:IndexClerk::isInUse,Logic: First Order Separation Logic, [code] requires:(unsigned int)index<(unsigned int)d_nextNewIndex ensures:(__out == false == > SEPEXISTS(0, d_unusedStack.size(), i, d_unus edStack[i] == index)) && (__out == true == > SEPFORALL(0, d_unusedStack. size(), i, d_unusedStack[i] != index))

  58. [58]

    Filename:bdld_datum.cpp,Function:DatumArrayRef::print,Logic: First Order Separa- tion Logic, [code] requires:stream.bad()||stream.good() ensures:__out == stream && (stream.bad() || (stream.good() && (SEPFORALL(0, d_length, i, stream + i7→d_data_p[i])) && stream.flushed()))

  59. [59]

    Filename:bdld_datum.cpp,Function:DatumMapEntry::print,Logic: First Order Sepa- ration Logic, [code] requires:!stream.bad() ensures:__out == stream && (stream.bad() || (stream.good() && (SEPFORALL(0, strlen(d_key_p), i, stream + i 7→ d_key_p[i]) ⋆ SEPFORALL(0, strlen(d_value), j, stream + strlen(d_key_p) + 1 + j7→d_value[j]))))

  60. [60]

    Filename:bdld_datumbinaryref.cpp,Function:DatumBinaryRef::print,Logic: First Order Separation Logic, [code] requires:stream.good() ensures:(stream.bad() == > __out == stream) && (stream.good() ==> (__out == (stream << bsl::flush) && (SEPFORALL(0, d_data_p.size(), i, stream + i 7→ d_ data_p[i]) ⋆ (stream + d_data_p.size() 7→ ’ ’)⋆ SEPFORALL(0, d_size.size(...

  61. [61]

    Filename:bdld_datummaker.cpp,Function:DatumMaker::operator(),Logic: First Order Separation Logic, [code] 19 requires:SEPFORALL(0, size, i, elements + i7→_) && size>= 0 ensures:__out == bdld::Datum::adoptMap(map) && (SEPFORALL(0, size, i, map.data()[i] == elements[i])⋆(*map.size() == size)⋆(*map.sorted() == sorted))

  62. [62]

    Filename:bdlde_base64alphabet.cpp,Function:Base64Alphabet::print,Logic: First Order Separation Logic, [code] requires:!stream.bad() && (value >= Base64Alphabet::Enum::MIN && value <= Base64Alphabet::Enum::MAX) ensures:__out == stream && (stream.bad() || (stream.good() && (SEPFORALL(0, strlen(Base64Alphabet::toAscii(value)), i, (stream + i) 7→ Base64Alphab...

  63. [63]

    Filename:bdlde_base64decoderoptions.cpp,Function:Base64DecoderOptions::print, Logic: First Order Separation Logic, [code] requires:stream.good() ensures:__out == stream && (SEPFORALL(0, 3, i, (__out + i 7→ sep_v && sep_ v == printer_attribute[i])))

  64. [64]

    Filename:bdlde_base64ignoremode.cpp,Function:Base64IgnoreMode::print,Logic: First Order Separation Logic, [code] requires:stream.good() ensures:__out == stream && (stream.bad() || (stream.good() && SEPFORALL(0, strlen(Base64IgnoreMode::toAscii(value)), i, (stream + i 7→ Base64IgnoreMode:: toAscii(value)[i]))))

  65. [65]

    Filename:bdlde_charconvertstatus.cpp,Function:CharConvertStatus::print,Logic: First Order Separation Logic, [code] requires:!stream.bad() ensures:__out == stream && (stream.bad() || (stream.good() && (SEPFORALL(0, strlen(CharConvertStatus::toAscii(value)), i, stream + i 7→ CharConvertStatus: :toAscii(value)[i]))))

  66. [66]

    Filename:bdlde_charconvertutf32.cpp,Function:decodeTwoOctets,Logic: First Order Separation Logic, [code] requires:SEPFORALL(0, 2, i, octBuf + i7→_) ensures:__out == ((octBuf[1] & ~k_CONTINUE_MASK) | ((octBuf[0] & ~k_ TWO_OCTET_MASK)<<k_CONTINUE_CONT_WID))

  67. [67]

    Filename:balm_metricformat.cpp,Function:MetricFormatSpec::formatValue,Logic: First Order Separation Logic, [code] requires:true ensures:__out == stream && (SEPFORALL(0, strlen(buffer), i, stream + i 7→ buffer[i]) || SEPFORALL(0, newBuffer.size(), i, stream + i 7→ newBuffer.data()[i]))

  68. [68]

    Filename:bdljsn_error.cpp,Function:bdljsn::operator <<,Logic: First Order Separa- tion Logic, [code] 20 requires:true ensures:__out == stream && (SEPFORALL(0, object.location().size(), i, stream + i 7→ object.location().data()[i]) ⋆ SEPFORALL(0, object.message().size(), j, stream + object.location().size() + j7→object.message().data()[j]))

  69. [69]

    Filename:bdljsn_jsontestsuiteutil.cpp,Function:getLeftBrackets100000,Logic: First Order Separation Logic, [code] requires:true ensures:__out != 0 && SEPFORALL(0, 100000, i, __out + i7→’[’)

  70. [70]

    Filename:baltzo_datafileloader.cpp,Function:validateTimeZoneId,Logic: First Order Separation Logic, [code] requires:timeZoneId != 0 && (timeZoneId[0] == ’/’ == > res_tmp == -

  71. [71]

    ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstu vwxyz1234567890/_+-

    && (SEPEXISTS(0, strlen(timeZoneId), i, (timeZoneId + i 7→ sep_v) && !bsl::strchr("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstu vwxyz1234567890/_+-", sep_v)) == > res_tmp == -2) && (SEPFORALL(0, strlen(timeZoneId), i, (timeZoneId + i 7→ sep_v) && bsl::strchr("ABCDEFGHIJK LMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz1234567890/_+-", sep_v)) ==>res_tmp == 0)...

  72. [72]

    Filename:baltzo_localdatetime.cpp,Function:baltzo::operator <<,Logic: First Order Separation Logic, [code] requires:true ensures:__out == stream && (stream.bad() || (stream.good() && (SEPFORALL(0, object.datetimeTz().size(), j, stream + j 7→ object.datetimeTz().data()[j]) ⋆ SEP- FORALL(0, object.timeZoneId().size(), i, stream + object.datetimeTz().size() ...

  73. [73]

    dstInEffectFlag().size(), j, stream + object.utcOffsetInSeconds().size() + j 7→ object

    Filename:baltzo_localtimedescriptor.cpp,Function:baltzo::operator <<,Logic: First Order Separation Logic, [code] requires:true ensures:__out == stream && (SEPFORALL(0, object.utcOffsetInSeconds().size(), i, stream + i 7→ object.utcOffsetInSeconds().data()[i]) ⋆ SEPFORALL(0, object. dstInEffectFlag().size(), j, stream + object.utcOffsetInSeconds().size() +...

  74. [74]

    Filename:bdlbb_blobutil.cpp,Function:asciiDumpFromBufferStart,Logic: First Order Separation Logic, [code] requires:0 <= bufferIndex && bufferIndex < source.numDataBuffers() && 0 <= numBytes && numBytes <= source.totalSize() - source.cumulativeSize(buffer 21 Index) ensures:__out == stream && (stream.bad() || (stream.good() && SEPFORALL(0, numBytes, i, stre...

  75. [75]

    Filename:bdlde_charconvertutf32.cpp,Function:decodeThreeOctets,Logic: First Order Separation Logic, [code] requires:SEPFORALL(0, 3, i, octBuf + i7→_) ensures:__out == ((octBuf[2] & ~k_CONTINUE_MASK) | ((octBuf[1] & ~k_ CONTINUE_MASK) << k_CONTINUE_CONT_WID) | ((octBuf[0] & ~k_THR EE_OCTET_MASK)<<(2 * k_CONTINUE_CONT_WID)))

  76. [76]

    Filename:bdlde_charconvertutf32.cpp,Function:decodeFourOctets,Logic: First Order Separation Logic, [code] requires:SEPFORALL(0, 4, i, octBuf + i7→_) ensures:__out == ((octBuf[3] & ~k_CONTINUE_MASK) | ((octBuf[2] & ~k_ CONTINUE_MASK) << k_CONTINUE_CONT_WID) | ((octBuf[1] & ~k_CON TINUE_MASK) << 2 * k_CONTINUE_CONT_WID) | ((octBuf[0] & ~k_FOU R_OCTET_MASK)<...

  77. [77]

    Filename:bdlde_charconvertutf32.cpp,Function:lookaheadContinuations,Logic: First Order Separation Logic, [code] requires:SEPFORALL(0, n, i, (octBuf + i7→_)) ensures:SEPFORALL(0, __out, i, (octBuf + i 7→ sep_v && isContinuation(sep_ v))) && (__out == n||!isContinuation(*(octBuf + __out)))

  78. [78]

    Filename:bdlde_crc32c.cpp,Function:calculateCrc32c,Logic: First Order Separation Logic, [code] requires:(length == 0)||(data != 0 && SEPFORALL(0, length, i, data + i7→_)) ensures:__out == crc

  79. [79]

    Filename:bdlde_sha2.cpp,Function:bdlde::operator==,Logic: First Order Separation Logic, [code] requires:lhs.d_bufferSize >= 0 && rhs.d_bufferSize >= 0 && SEPFORALL(0, lhs.d_bufferSize, i, lhs.d_buffer + i 7→ _) && SEPFORALL(0, rhs.d_bufferSize, i, rhs.d_buffer + i 7→ _) && SEPFORALL(0, 8, i, lhs.d_state + i 7→ _) && SEP- FORALL(0, 8, i, rhs.d_state + i7→_...

  80. [80]

    Filename:bdlde_utf8util.cpp,Function:get4ByteValue,Logic: First Order Separation Logic, [code] 22 requires:SEPFORALL(0, 4, i, pc + i7→_) ensures:__out == ((*pc & 0x7) << 18) | ((pc[1] & k_CONT_V ALUE_MASK) << 12) | ((pc[2] & k_CONT_V ALUE_MASK)<< 6) | (pc[3] & k_CONT_V ALUE _MASK)

Showing first 80 references.